English
Automorphization distributes over left scalar multiplication in quotient groups: automorphize ((g ∘ Quotient.mk') • f) = g • automorphize f.
Русский
Автоматизизация распределяется по левому умножению на скаляр в факторгруппах: automorphize((g ∘ Quotient.mk') • f) = g • automorphize f.
LaTeX
$$$\\operatorname{QuotientGroup}.automorphize ((g \\circ Quotient.mk') \\cdot f) = g \\cdot (\\operatorname{QuotientGroup}.automorphize f)$$$
Lean4
@[to_additive]
theorem even_mul_odd {f : ℕ → M} (he : HasProd (fun k ↦ f (2 * k)) m) (ho : HasProd (fun k ↦ f (2 * k + 1)) m') :
HasProd f (m * m') := by
have := mul_right_injective₀ (two_ne_zero' ℕ)
replace ho := ((add_left_injective 1).comp this).hasProd_range_iff.2 ho
refine (this.hasProd_range_iff.2 he).mul_isCompl ?_ ho
simpa [Function.comp_def] using Nat.isCompl_even_odd
