English
The real numbers carry a commutative ring structure under the usual addition and multiplication.
Русский
Действительные числа обладают коммутативной кольцевой структурой под обычными операциями сложения и умножения.
LaTeX
$$$\text{Real is a commutative ring under } (+, \cdot, 0, 1)$$$
Lean4
instance commRing : CommRing ℝ where
natCast n := ⟨n⟩
intCast z := ⟨z⟩
zero := (0 : ℝ)
one := (1 : ℝ)
mul := (· * ·)
add := (· + ·)
neg := @Neg.neg ℝ _
sub := @Sub.sub ℝ _
npow := @npowRec ℝ ⟨1⟩ ⟨(· * ·)⟩
nsmul := @nsmulRec ℝ ⟨0⟩ ⟨(· + ·)⟩
zsmul := @zsmulRec ℝ ⟨0⟩ ⟨(· + ·)⟩ ⟨@Neg.neg ℝ _⟩ (@nsmulRec ℝ ⟨0⟩ ⟨(· + ·)⟩)
add_zero a := by apply ext_cauchy; simp [cauchy_add, cauchy_zero]
zero_add a := by apply ext_cauchy; simp [cauchy_add, cauchy_zero]
add_comm a b := by apply ext_cauchy; simp only [cauchy_add, add_comm]
add_assoc a b c := by apply ext_cauchy; simp only [cauchy_add, add_assoc]
mul_zero a := by apply ext_cauchy; simp [cauchy_mul, cauchy_zero]
zero_mul a := by apply ext_cauchy; simp [cauchy_mul, cauchy_zero]
mul_one a := by apply ext_cauchy; simp [cauchy_mul, cauchy_one]
one_mul a := by apply ext_cauchy; simp [cauchy_mul, cauchy_one]
mul_comm a b := by apply ext_cauchy; simp only [cauchy_mul, mul_comm]
mul_assoc a b c := by apply ext_cauchy; simp only [cauchy_mul, mul_assoc]
left_distrib a b c := by apply ext_cauchy; simp only [cauchy_add, cauchy_mul, mul_add]
right_distrib a b c := by apply ext_cauchy; simp only [cauchy_add, cauchy_mul, add_mul]
neg_add_cancel a := by apply ext_cauchy; simp [cauchy_add, cauchy_neg, cauchy_zero]
natCast_zero := by apply ext_cauchy; simp [cauchy_zero]
natCast_succ n := by apply ext_cauchy; simp [cauchy_one, cauchy_add]
intCast_negSucc z := by apply ext_cauchy; simp [cauchy_neg, cauchy_natCast]
