instAddMonoidWithOne — Mathlib

English

The natural-number embedding into a product α × β is given componentwise by n ↦ (n, n).

Русский

Естественное впрыскивание ℕ в произведение α × β задано диагонально: n ↦ (n, n).

LaTeX

$$$ \text{natCast}_{\alpha \times \beta}(n) = (n,n) $$$

Lean4

instance instAddMonoidWithOne : AddMonoidWithOne (α × β) :=
  { Prod.instAddMonoid,
    @Prod.instOne α β _ _ with
    natCast := fun n => (n, n)
    natCast_zero := congr_arg₂ Prod.mk Nat.cast_zero Nat.cast_zero
    natCast_succ := fun _ => congr_arg₂ Prod.mk (Nat.cast_succ _) (Nat.cast_succ _) }

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