English
The star conjugation starAe is an algebra equivalence between H and its opposite, given by star then mapping to the opposite ring.
Русский
Звездная конъюгация starAe — это алгебраическое эквалентство между H и его противоположной:ring, заданное конъюгацией star и отображением в противоположную.
LaTeX
$$$\text{starAe} : \mathbb{H}(R,c_1,c_2,c_3) \cong_{\mathbb{R}} \mathbb{H}(R,c_1,c_2,c_3)^{\mathrm{op}} \,\text{ с }\text{toFun} = \mathrm{op} \circ \star \text{ и }\text{invFun} = \star \circ \mathrm{unop}$$$
Lean4
/-- Quaternion conjugate as an `AlgEquiv` to the opposite ring. -/
def starAe : ℍ[R,c₁,c₂,c₃] ≃ₐ[R] ℍ[R,c₁,c₂,c₃]ᵐᵒᵖ :=
{ starAddEquiv.trans opAddEquiv with
toFun := op ∘ star
invFun := star ∘ unop
map_mul' := fun x y => by simp
commutes' := fun r => by simp }
