English
The complex numbers form a commutative ring.
Русский
Комплексные числа образуют коммутативное кольцо.
LaTeX
$$$\mathbb{C} \text{ is a commutative ring}$$$
Lean4
instance commRing : CommRing ℂ :=
{ addGroupWithOne with
mul := (· * ·)
npow := @npowRec _ ⟨(1 : ℂ)⟩ ⟨(· * ·)⟩
add_comm := by intros; ext <;> simp <;> ring
left_distrib := by intros; ext <;> simp [mul_re, mul_im] <;> ring
right_distrib := by intros; ext <;> simp [mul_re, mul_im] <;> ring
zero_mul := by intros; ext <;> simp
mul_zero := by intros; ext <;> simp
mul_assoc := by intros; ext <;> simp <;> ring
one_mul := by intros; ext <;> simp
mul_one := by intros; ext <;> simp
mul_comm := by intros; ext <;> simp <;> ring }
