English
Properties showing that for S-torsion', the construction is compatible with SMul and addition, illustrating closure under addition and scalar action by S.
Русский
Свойства, демонстрирующие, что для torsion' свойства сохраняются при сложении и умножении на элементы S, иллюстрируя замкнутость по сложению и скалярам S.
LaTeX
$$proof of closure properties for torsion' (omitted)$$
Lean4
/-- The `S`-torsion submodule, containing all elements `x` of `M` such that `a • x = 0` for some
`a` in `S`. -/
@[simps!]
def torsion' (S : Type*) [CommMonoid S] [DistribMulAction S M] [SMulCommClass S R M] : Submodule R M
where
carrier := {x | ∃ a : S, a • x = 0}
add_mem' := by
intro x y ⟨a, hx⟩ ⟨b, hy⟩
use b * a
rw [smul_add, mul_smul, mul_comm, mul_smul, hx, hy, smul_zero, smul_zero, add_zero]
zero_mem' := ⟨1, smul_zero 1⟩
smul_mem' := fun a x ⟨b, h⟩ => ⟨b, by rw [smul_comm, h, smul_zero]⟩
