isTorsionBySet_iff_subseteq_ker_lsmul

English

IsTorsionBySet s is equivalent to s being contained in the kernel of the left scalar multiplication map.

Русский

IsTorsionBySet s эквивалентно тому, что s ⊆ ker(lsmul).

LaTeX

$$$IsTorsionBySet\,R\,M\,s \;\iff\; s \subseteq \ker(\mathrm{LinearMap}.lsmul\,R\,M)$$$

Lean4

theorem isTorsionBySet_iff_subseteq_ker_lsmul : IsTorsionBySet R M s ↔ s ⊆ LinearMap.ker (LinearMap.lsmul R M)
    where
  mp h r hr := LinearMap.mem_ker.mpr <| LinearMap.ext fun x => @h x ⟨r, hr⟩
  mpr
    | h, x, ⟨_, hr⟩ => DFunLike.congr_fun (LinearMap.mem_ker.mp (h hr)) x

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