im_ofNat

Mathlib.Algebra.QuadraticAlgebra

URI: https://scilib.ai/kg/mathlib#QuadraticAlgebra.im_ofNat

English

For every natural n with n ≥ 2, the imaginary part of ofNat(n) in QuadraticAlgebra is 0.

Русский

Для любого натурального n, n ≥ 2, мнимая часть образа ofNat(n) в QuadraticAlgebra равна 0.

LaTeX

$$$[n\in\mathbb{N},\ n\ge 2]\implies (\mathrm{im}\,\mathrm{ofNat}(n)) = 0$$$

Lean4

@[scoped simp]
theorem im_ofNat (n : ℕ) [n.AtLeastTwo] : (ofNat(n) : QuadraticAlgebra R a b).im = 0 :=
  rfl

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

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

Разделы

Аффилиация

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