English
The lift of a symmetric, bilinear-like operation interacts with scalar multiplication in a bilinear fashion: the product of lifts equals the lift of the pointwise product.
Русский
Лифт двух симметричных билинейных отображений совместим с умножением: произведение лофов равняется лофу покомпонентного произведения.
LaTeX
$$$\\forall {\\alpha} {R} {N} \\ [\\mathrm{SMul}\\ R\\ N] \\, (f : \\{ f : \\alpha \\to \\alpha \\to R \\mid \\forall a_1 a_2, f\\,a_1\\,a_2 = f\\,a_2\\,a_1}) \\, (g : { g : \\alpha \\to \\alpha \\to N \\mid \\forall a_1 a_2, g\\,a_1\\,a_2 = g\\,a_2\\,a_1}) \\, : \\, \\mathrm{lift} f \\cdot \\mathrm{lift} g = \\mathrm{lift}\\langle f.\\mathrm{val} \\cdot g.\\mathrm{val}, \\ \\text{proof} \\rangle$$$
Lean4
theorem lift_smul_lift {α R N} [SMul R N] (f : { f : α → α → R // ∀ a₁ a₂, f a₁ a₂ = f a₂ a₁ })
(g : { g : α → α → N // ∀ a₁ a₂, g a₁ a₂ = g a₂ a₁ }) :
lift f • lift g =
lift
⟨f.val • g.val, fun _ _ => by
rw [Pi.smul_apply', Pi.smul_apply', Pi.smul_apply', Pi.smul_apply', f.prop, g.prop]⟩ :=
by
ext ⟨i, j⟩
simp_all only [Pi.smul_apply', lift_mk]
