instNatCast — Mathlib

English

Natural numbers embed into 𝓜(𝕜, A) compatibly with the product representation: (n : 𝓜(𝕜, A)).toProd = n.cast.toProd.

Русский

Естественные числа встроены в 𝓜(𝕜, A) совместно с представлением в произведении: (n : 𝓜(𝕜, A)).toProd = n.cast.toProd.

LaTeX

$$$ (n : 𝓜(𝕜, A)).toProd = n.cast.toProd $$$

Lean4

instance instNatCast : NatCast 𝓜(𝕜, A) where
  natCast
    n :=
    ⟨n, fun x y => by
      rw [Prod.snd_natCast, Prod.fst_natCast]
      simp only [← Nat.smul_one_eq_cast, smul_apply, one_apply, mul_smul_comm, smul_mul_assoc]⟩

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