English
Complex conjugation is a ring involution on ℂ: for all a,b ∈ ℂ, conj(a b) = conj a conj b, conj(a+b) = conj a + conj b, and conj(conj z) = z.
Русский
Сопряжение является инвольтивным автоморфизмом кольца ℂ: для всех a,b ∈ ℂ выполняются conj(ab) = conj(a) conj(b), conj(a+b) = conj(a) + conj(b), и conj(conj z) = z.
LaTeX
$$$(\forall a,b \in \mathbb{C}, \overline{a b} = \overline{a}\,\overline{b}) \land (\forall a,b \in \mathbb{C}, \overline{a+b} = \overline{a} + \overline{b}) \land (\forall z \in \mathbb{C}, \overline{\overline{z}} = z)$$$
Lean4
/-- This defines the complex conjugate as the `star` operation of the `StarRing ℂ`. It
is recommended to use the ring endomorphism version `starRingEnd`, available under the
notation `conj` in the scope `ComplexConjugate`. -/
instance : StarRing ℂ where
star z := ⟨z.re, -z.im⟩
star_involutive x := by simp only [eta, neg_neg]
star_mul a b := by ext <;> simp [add_comm] <;> ring
star_add a b := by ext <;> simp [add_comm]
