English
A module over a domain has NoZeroSMulDivisors iff its torsion is bot.
Русский
Модуль над доменом имеет NoZeroSMulDivisors тогда и только тогда, когда тorsion равен ⊥.
LaTeX
$$NoZeroSMulDivisors R M ↔ torsion R M = ⊥$$
Lean4
/-- A module over a domain has `NoZeroSMulDivisors` iff its torsion submodule is trivial. -/
theorem noZeroSMulDivisors_iff_torsion_eq_bot : NoZeroSMulDivisors R M ↔ torsion R M = ⊥ :=
by
constructor <;> intro h
· haveI : NoZeroSMulDivisors R M := h
rw [eq_bot_iff]
rintro x ⟨a, hax⟩
change (a : R) • x = 0 at hax
rcases eq_zero_or_eq_zero_of_smul_eq_zero hax with h0 | h0
· exfalso
exact nonZeroDivisors.coe_ne_zero a h0
· exact h0
·
exact
{
eq_zero_or_eq_zero_of_smul_eq_zero := fun {a} {x} hax =>
by
by_cases ha : a = 0
· left
exact ha
· right
rw [← mem_bot R, ← h]
exact ⟨⟨a, mem_nonZeroDivisors_of_ne_zero ha⟩, hax⟩ }
