R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑(annihilator ⊤)
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors (annihilator ⊤)))
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors (annihilator ⊤)))
have hM' := Module.isTorsionBySet_annihilator_top R M
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑(annihilator ⊤)
hI : ↑(annihilator ⊤) ∩ ↑(nonZeroDivisors R) ≠ ∅
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors (annihilator ⊤)))
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑(annihilator ⊤)
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors (annihilator ⊤)))
have hI := Submodule.annihilator_top_inter_nonZeroDivisors hM
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑(annihilator ⊤)
hI : ↑(annihilator ⊤) ∩ ↑(nonZeroDivisors R) ≠ ∅
⊢ annihilator ⊤ ≠ ⊥
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑(annihilator ⊤)
hI : ↑(annihilator ⊤) ∩ ↑(nonZeroDivisors R) ≠ ∅
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors (annihilator ⊤)))
refine' isInternal_prime_power_torsion_of_is_torsion_by_ideal _ hM'
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑(annihilator ⊤)
hI : Set.Nonempty (↑(annihilator ⊤) ∩ ↑(nonZeroDivisors R))
⊢ annihilator ⊤ ≠ ⊥
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑(annihilator ⊤)
hI : ↑(annihilator ⊤) ∩ ↑(nonZeroDivisors R) ≠ ∅
⊢ annihilator ⊤ ≠ ⊥
rw [← Set.nonempty_iff_ne_empty] at hI
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑(annihilator ⊤)
hI : Set.Nonempty (↑(annihilator ⊤) ∩ ↑(nonZeroDivisors R))
⊢ ∃ x, x ∈ annihilator ⊤ ∧ x ≠ 0
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑(annihilator ⊤)
hI : Set.Nonempty (↑(annihilator ⊤) ∩ ↑(nonZeroDivisors R))
⊢ annihilator ⊤ ≠ ⊥
rw [Submodule.ne_bot_iff]
case intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑(annihilator ⊤)
x : R
H : x ∈ ↑(annihilator ⊤)
hx : x ∈ ↑(nonZeroDivisors R)
⊢ ∃ x, x ∈ annihilator ⊤ ∧ x ≠ 0
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑(annihilator ⊤)
hI : Set.Nonempty (↑(annihilator ⊤) ∩ ↑(nonZeroDivisors R))
⊢ ∃ x, x ∈ annihilator ⊤ ∧ x ≠ 0
obtain ⟨x, H, hx⟩ := hI
no goals
case intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑(annihilator ⊤)
x : R
H : x ∈ ↑(annihilator ⊤)
hx : x ∈ ↑(nonZeroDivisors R)
⊢ ∃ x, x ∈ annihilator ⊤ ∧ x ≠ 0
exact ⟨x, H, nonZeroDivisors.ne_zero hx⟩