re_ofNat

Mathlib.Algebra.QuadraticAlgebra

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

English

The real part of ofNat(n) in QuadraticAlgebra R a b is exactly ofNat(n).

Русский

Действительная часть ofNat(n) в QuadraticAlgebra R a b равна ofNat(n).

LaTeX

$$$\\text{re}(\\text{ofNat}(n) : QuadraticAlgebra R a b) = \\text{ofNat}(n)$$$

Lean4

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

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

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

Разделы

Аффилиация

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