instSMul — Mathlib

English

There is a canonical SMul action of Submodule R A on Submodule R M, compatible with all structures.

Русский

Существует каноническое действие SMul Submodule R A на Submodule R M, согласованное со всеми структурами.

LaTeX

$$$\\text{SMul} : (\\text{Submodule } R A) \\to (\\text{Submodule } R M) \\to \\text{SMul}$$$

Lean4

instance : SMul (Submodule R A) (Submodule R M) where
  smul A'
    M' :=
    { __ := A'.toAddSubmonoid • M'.toAddSubmonoid
      smul_mem' := fun r m hm ↦
        AddSubmonoid.smul_induction_on hm
          (fun a ha m hm ↦ by rw [← smul_assoc]; exact AddSubmonoid.smul_mem_smul (A'.smul_mem r ha) hm)
          fun m₁ m₂ h₁ h₂ ↦ by rw [smul_add]; exact (A'.1 • M'.1).add_mem h₁ h₂ }

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