automorphize_smul_left — Mathlib

English

Automorphization distributes over left scalar multiplication on a quotient by an additive subgroup: (QuotientAddGroup.automorphize ( (g ∘ Quotient.mk') • f )) = g • QuotientAddGroup.automorphize f.

Русский

Автоматизизация в отношении ADD-группы: automorphize( (g ∘ quotient.mk') • f) = g • automorphize f.

LaTeX

$$$\\operatorname{QuotientAddGroup}.automorphize ((g \\circ (Quotient.mk')) \\cdot f) = g \\cdot (\\operatorname{QuotientAddGroup}.automorphize f)$$$

Lean4

/-- Automorphization of a function into an `R`-`Module` distributes, that is, commutes with the
`R`-scalar multiplication. -/
theorem automorphize_smul_left (f : G → M) (g : G ⧸ Γ → R) :
    QuotientAddGroup.automorphize ((g ∘ (@Quotient.mk' _ (_))) • f) =
      g • (QuotientAddGroup.automorphize f : G ⧸ Γ → M) :=
  AddAction.automorphize_smul_left f g

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