annihilator_top_inter_nonZeroDivisors

English

In a domain, NoZeroSMulDivisors is equivalent to torsion being bot after quotient.

Русский

В области (domain) NoZeroSMulDivisors эквивалентно тому, что при квартиовании тorsion становится ⊥.

LaTeX

$$NoZeroSMulDivisors R M ↔ torsion R M = ⊥$$

Lean4

theorem _root_.Submodule.annihilator_top_inter_nonZeroDivisors [Module.Finite R M] (hM : Module.IsTorsion R M) :
    ((⊤ : Submodule R M).annihilator : Set R) ∩ R⁰ ≠ ∅ :=
  by
  obtain ⟨S, hS⟩ := ‹Module.Finite R M›.fg_top
  refine Set.Nonempty.ne_empty ⟨_, ?_, (∏ x ∈ S, (@hM x).choose : R⁰).prop⟩
  rw [Submonoid.coe_finset_prod, SetLike.mem_coe, ← hS, mem_annihilator_span]
  intro n
  letI := Classical.decEq M
  rw [← Finset.prod_erase_mul _ _ n.prop, mul_smul, ← Submonoid.smul_def, (@hM n).choose_spec, smul_zero]

Похожие утверждения