coe_one — Mathlib

English

Let EReal be the extended real numbers and consider the natural embedding of the real numbers into EReal. Then the image of 1 from the real numbers equals the unit 1 in EReal.

Русский

Пусть EReal — расширенные вещественные числа и имеется естественное вложение ℝ в EReal. Тогда образ числа 1 из ℝ в EReal равен единице в EReal.

LaTeX

$$$((1 : \mathbb{R}) : \mathrm{EReal}) = 1$$$

Lean4

@[simp, norm_cast]
theorem coe_one : ((1 : ℝ) : EReal) = 1 :=
  rfl

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