addGroupWithOne — Mathlib

English

The complex numbers form a ring under the usual addition and multiplication, with 1 as the multiplicative identity.

Русский

Комплексные числа образуют кольцо под обычными операциями сложения и умножения, единица служит единицей умножения.

LaTeX

$$$\mathbb{C} \text{ is a ring}$$$

Lean4

instance addGroupWithOne : AddGroupWithOne ℂ :=
  { Complex.addCommGroup with
    natCast_zero := by ext <;> simp
    natCast_succ _ := by ext <;> simp
    intCast_ofNat _ := by ext <;> simp
    intCast_negSucc _ := by ext <;> simp
    one := 1 }

Похожие утверждения