coe_ofNat — Mathlib

English

For every natural number n, the natural embedding of n into R and then into the quaternion algebra equals the direct embedding of n into the quaternion algebra: ((ofNat(n) : R) : ℍ[R,c₁,c₂,c₃]) = (ofNat(n) : ℍ[R,c₁,c₂,c₃]).

Русский

Для каждого натурального числа n вложение n в R и далее в кватернионову алгебру совпадает с прямым вложением n в кватернионову алгебру.

LaTeX

$$$((\mathrm{ofNat}(n) : R) : \mathbb{H}(R;c_1,c_2,c_3)) = (\mathrm{ofNat}(n) : \mathbb{H}(R;c_1,c_2,c_3)).$$$

Lean4

@[norm_cast, simp]
theorem coe_ofNat {n : ℕ} [n.AtLeastTwo] : ((ofNat(n) : R) : ℍ[R,c₁,c₂,c₃]) = (ofNat(n) : ℍ[R,c₁,c₂,c₃]) :=
  rfl

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