ofReal_injective

Mathlib.Analysis.RCLike.Basic

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

English

The embedding of real numbers into K is injective: z ↦ z is preserved.

Русский

Встраивание ℝ в K инъективно: z ↦ z сохраняется.

LaTeX

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

Lean4

theorem ofReal_injective : Function.Injective ((↑) : ℝ → K) :=
  (algebraMap ℝ K).injective

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

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

Разделы

Аффилиация

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