English
The map x ↦ complexConj_K(x) defines a star operation on the field K, turning K into a star ring with involutive, multiplicative, and additive properties preserved by complex conjugation.
Русский
Отображение x ↦ complexConj_K(x) задаёт на поле K операцию звезды, превращающую K в звездное кольцо; сопряжение является инволютивным и сохраняет сложение и умножение (в связке с коммутативностью).
LaTeX
$$$\\star: K \\to K, \\; \\star(x)=\\mathrm{complexConj}_K(x),$ with $\\star(xy)=\\star(x)\\star(y)$ and $\\star(x+y)=\\star(x)+\\star(y)$ and $\\star(\\star(x))=x$$$
Lean4
noncomputable instance starRing : StarRing K where
star := complexConj K
star_involutive _ := complexConj_apply_apply _ _
star_mul _ _ := by rw [map_mul, mul_comm]
star_add _ _ := by rw [map_add]
