toReal_injective

Mathlib.NumberTheory.Zsqrtd.ToReal

URI: https://scilib.ai/kg/mathlib#Zsqrtd.toReal_injective

English

The map toReal h0d is injective provided h0d ≥ 0 and hd(n) ≠ 0 for all n ≠ 0.

Русский

Отображение toReal является инъективным при условии h0d ≥ 0 и hd(n) ≠ 0 для всех n ≠ 0.

LaTeX

$$$ \text{toReal}_{d} \text{ injective under given conditions} $$$

Lean4

theorem toReal_injective {d : ℤ} (h0d : 0 ≤ d) (hd : ∀ n : ℤ, d ≠ n * n) : Function.Injective (toReal h0d) :=
  lift_injective _ hd

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

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

Разделы

Аффилиация

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