English
Z[√d] is a star ring: there is an involution star that reverses multiplication and preserves addition, with star(star(z)) = z.
Русский
Z[√d] образует звездообразную кольцевую структуру: существует отображение сопряжения, являющееся инволюцией, обращающее произведение и сохраняющее сложение, и звезда от звезды возвращает исходное.
LaTeX
$$$$ \text{star is an involutive anti-automorphism: } (xy)^{*} = y^{*}x^{*}, \ (x+y)^{*} = x^{*}+y^{*}, \ (z^{*})^{*} = z. $$$$
Lean4
instance : StarRing (ℤ√d) where
star_involutive _ := Zsqrtd.ext rfl (neg_neg _)
star_mul a b := by ext <;> simp <;> ring
star_add _
_ :=
Zsqrtd.ext rfl
(neg_add _ _)
-- Porting note: proof was `by decide`
