English
The additive homomorphism toProdHom preserves addition: toProdHom(a+b) = toProdHom(a) + toProdHom(toProdHom(b)).
Русский
Гомоморфизм toProdHom сохраняет сложение: toProdHom(a+b) = toProdHom(a) + toProdHom(b).
LaTeX
$$$\\mathrm{toProdHom}(a+b) = \\mathrm{toProdHom}(a) + \\mathrm{toProdHom}(b)$$$
Lean4
/-- The star operation on `a : 𝓜(𝕜, A)` is given by
`(star a).toProd = (star ∘ a.snd ∘ star, star ∘ a.fst ∘ star)`. -/
instance instStar : Star 𝓜(𝕜, A) where
star
a :=
{ fst := (((starₗᵢ 𝕜 : A ≃ₗᵢ⋆[𝕜] A) : A →L⋆[𝕜] A).comp a.snd).comp ((starₗᵢ 𝕜 : A ≃ₗᵢ⋆[𝕜] A) : A →L⋆[𝕜] A)
snd := (((starₗᵢ 𝕜 : A ≃ₗᵢ⋆[𝕜] A) : A →L⋆[𝕜] A).comp a.fst).comp ((starₗᵢ 𝕜 : A ≃ₗᵢ⋆[𝕜] A) : A →L⋆[𝕜] A)
central := fun x y => by
simpa only [star_mul, star_star] using (congr_arg star (a.central (star y) (star x))).symm }
