case h
R : Type u_2
M : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : M
⊢ x ∈ ↑(torsion R M) ↔ x ∈ {x | annihilator (span R {x}) ≠ ⊥}
R : Type u_2
M : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ ↑(torsion R M) = {x | annihilator (span R {x}) ≠ ⊥}
ext x
case h
R : Type u_2
M : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : M
⊢ x ∈ ↑(torsion R M) ↔ x ∈ {x | ∃ x_1, (∀ (n : M), (∃ a, a • x = n) → x_1 • n = 0) ∧ x_1 ≠ 0}
case h
R : Type u_2
M : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : M
⊢ x ∈ ↑(torsion R M) ↔ x ∈ {x | annihilator (span R {x}) ≠ ⊥}
simp_rw [Submodule.ne_bot_iff, mem_annihilator, mem_span_singleton]
no goals
case h
R : Type u_2
M : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : M
⊢ x ∈ ↑(torsion R M) ↔ x ∈ {x | ∃ x_1, (∀ (n : M), (∃ a, a • x = n) → x_1 • n = 0) ∧ x_1 ≠ 0}
exact
  ⟨fun ⟨a, hax⟩ =>
    ⟨a, fun _ ⟨b, hb⟩ => by rw [← hb, smul_comm, ← Submonoid.smul_def, hax, smul_zero],
      nonZeroDivisors.coe_ne_zero _⟩,
    fun ⟨a, hax, ha⟩ => ⟨⟨_, mem_nonZeroDivisors_of_ne_zero ha⟩, hax x ⟨1, one_smul _ _⟩⟩⟩
no goals
R : Type u_2
M : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : M
x✝² : x ∈ ↑(torsion R M)
a : { x // x ∈ R⁰ }
hax : a • x = 0
x✝¹ : M
x✝ : ∃ a, a • x = x✝¹
b : R
hb : b • x = x✝¹
⊢ ↑a • x✝¹ = 0
rw [← hb, smul_comm, ← Submonoid.smul_def, hax, smul_zero]