English
The real numbers form a field under the usual addition and multiplication.
Русский
Числа ℝ образуют поле по обычным операциям сложения и умножения.
LaTeX
$$$\mathbb{R} \text{ is a field}$$$
Lean4
noncomputable instance instField : Field ℝ
where
mul_inv_cancel := by
rintro ⟨a⟩ h
rw [mul_comm]
simp only [← ofCauchy_inv, ← ofCauchy_mul, ← ofCauchy_one, ← ofCauchy_zero, Ne, ofCauchy.injEq] at *
exact CauSeq.Completion.inv_mul_cancel h
inv_zero := by simp [← ofCauchy_zero, ← ofCauchy_inv]
nnqsmul := _
nnqsmul_def := fun _ _ => rfl
qsmul := _
qsmul_def := fun _ _ => rfl
nnratCast_def q := by rw [← ofCauchy_nnratCast, NNRat.cast_def, ofCauchy_div, ofCauchy_natCast, ofCauchy_natCast]
ratCast_def
q := by
rw [← ofCauchy_ratCast, Rat.cast_def, ofCauchy_div, ofCauchy_natCast, ofCauchy_intCast]
-- Extra instances to short-circuit type class resolution
