instIntCast — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance instIntCast : IntCast 𝓜(𝕜, A) where
  intCast
    n :=
    ⟨n, fun x y => by
      rw [Prod.snd_intCast, Prod.fst_intCast]
      simp only [← Int.smul_one_eq_cast, smul_apply, one_apply, mul_smul_comm, smul_mul_assoc]⟩

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