coe_natCast — Mathlib

English

The natural embedding from the ring R into the quaternion algebra preserves the natural numbers: the coercion of n from R equals the quaternion n.

Русский

Естественное вложение из кольца R в алгебру кватернионов сохраняет натуральные числа: вложение n из R равно кватерниону n.

LaTeX

$$$\uparrow( n ) = ( n \text{ in } \mathbb{H})$$$

Lean4

@[norm_cast]
theorem coe_natCast (n : ℕ) : ↑(n : R) = (n : ℍ[R,c₁,c₂,c₃]) :=
  rfl

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