English
The torsion by any set coincides with the torsion by the ideal generated by that set: torsionBySet(R, M, s) = torsionBySet(R, M, Ideal.span s).
Русский
Торион по множеству совпадает с торионом по идеалу, порожденному этим множеством: torsionBySet(R, M, s) = torsionBySet(R, M, Ideal.span s).
LaTeX
$$$\mathrm{torsionBySet}\,R\,M\,s = \mathrm{torsionBySet}\,R\,M\,\big(\mathrm{Ideal}.\mathrm{span}\,s\big)$$$
Lean4
/-- Torsion by a set is torsion by the ideal generated by it. -/
theorem torsionBySet_eq_torsionBySet_span : torsionBySet R M s = torsionBySet R M (Ideal.span s) :=
by
refine le_antisymm (fun x hx => ?_) (torsionBySet_le_torsionBySet_of_subset subset_span)
rw [mem_torsionBySet_iff] at hx ⊢
suffices Ideal.span s ≤ Ideal.torsionOf R M x by
rintro ⟨a, ha⟩
exact this ha
rw [Ideal.span_le]
exact fun a ha => hx ⟨a, ha⟩
