ofReal_one

Mathlib.Analysis.RCLike.Basic

URI: https://scilib.ai/kg/mathlib#RCLike.ofReal_one

English

The embedding of real numbers into K is injective: if (z : K) = (w : K) then z = w for z,w ∈ ℝ.

Русский

Встраивание действительных чисел в K является инъективным: если (z : K) = (w : K), то z = w для z,w ∈ ℝ.

LaTeX

$$$\forall z,w \in \mathbb{R},\ (z:K) = (w:K) \Rightarrow z = w$$$

Lean4

@[norm_cast]
theorem ofReal_one : ((1 : ℝ) : K) = 1 :=
  map_one (algebraMap ℝ K)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru