English
The auxiliary lift applied to the bilinear embedding of even generators equals the bilin map of f.
Русский
Применение вспомогательного подъема к би-линейному вложению чётных генераторов даёт bilinear отображение f.
LaTeX
$$lift_aux_ι: even.lift.aux f ((even.ι Q).bilin m1 m2) = f.bilin m1 m2$$
Lean4
@[simp]
theorem aux_mul (x y : even Q) : aux f (x * y) = aux f x * aux f y :=
by
obtain ⟨x, x_property⟩ := x
cases y
refine (congr_arg Prod.fst (foldr_mul _ _ _ _ _ _)).trans ?_
dsimp only
induction x, x_property using even_induction Q with
| algebraMap r =>
generalize_proofs at ⊢
simpa using Algebra.smul_def r _
| add x y hx hy ihx ihy =>
rw [LinearMap.map_add, Prod.fst_add]
simp [ihx, ihy, ← add_mul, ← LinearMap.map_add]
| ι_mul_ι_mul m₁ m₂ x hx ih => simp [aux_apply, ih, ← mul_assoc]
