coe_ofNat — Mathlib

English

For any n, the real part of the natural embedding of n into QuadraticAlgebra R a b is exactly n.

Русский

Для любого n действительная часть натурального внедрения n в QuadraticAlgebra R a b равна именно n.

LaTeX

$$$\\operatorname{re}((\\mathrm{ofNat}\\! (n) : \\ QuadraticAlgebra R a b)) = \\mathrm{ofNat}\\! (n)$$$

Lean4

@[simp, norm_cast]
theorem coe_ofNat (n : ℕ) [n.AtLeastTwo] :
    ((ofNat(n) : R) : QuadraticAlgebra R a b) = (ofNat(n) : QuadraticAlgebra R a b) := by ext <;> rfl

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