lift'_smul — Mathlib

English

The lift' commutes with scalar multiplication by R: r • lift'(m) = lift'(r • m).

Русский

lift' коммутирует с действием скаляра: r • lift'(m) = lift'(r • m).

LaTeX

$$$\\forall r\\in R:\\ \\mathrm{lift}'(g,h)(r\\cdot m) = r\\cdot \\mathrm{lift}'(g,h)(m).$$$

Lean4

theorem lift'_smul (g : M →ₗ[R] M'') (h : ∀ x : S, IsUnit ((algebraMap R (Module.End R M'')) x)) (r : R) (m) :
    r • LocalizedModule.lift' S g h m = LocalizedModule.lift' S g h (r • m) :=
  m.induction_on fun a b => by
    rw [LocalizedModule.lift'_mk, LocalizedModule.smul'_mk, LocalizedModule.lift'_mk, ← map_smul, ← g.map_smul]

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