English
Automorphization distributes over left scalar multiplication on a quotient by a subgroup: (QuotientGroup.automorphize ( (g ∘ Quotient.mk') • f )) = g • QuotientGroup.automorphize f.
Русский
Автоматизизация распределяется по левому умножению на скаляр: (QuotientGroup.automorphize( (g ∘ Quotient.mk') • f )) = g • QuotientGroup.automorphize f.
LaTeX
$$$\\operatorname{QuotientGroup}.automorphize ((g \\circ \\mathrm{Quotient.mk}') \\cdot f) = g \\cdot (\\operatorname{QuotientGroup}.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) :
(QuotientGroup.automorphize ((g ∘ (@Quotient.mk' _ (_)) : G → R) • f) : G ⧸ Γ → M) =
g • (QuotientGroup.automorphize f : G ⧸ Γ → M) :=
MulAction.automorphize_smul_left f g
