Documentation

Mathlib.Data.Nat.Cast.Prod

The product of two AddMonoidWithOnes. #

source
instance Prod.instAddMonoidWithOne {α : Type u_1} {β : Type u_2} [AddMonoidWithOne α] [AddMonoidWithOne β] :
AddMonoidWithOne (α × β)
Equations
    source
    @[simp]
    theorem Prod.fst_natCast {α : Type u_1} {β : Type u_2} [AddMonoidWithOne α] [AddMonoidWithOne β] (n : ℕ) :
    (↑n).1 = ↑n
    source
    @[simp]
    theorem Prod.fst_ofNat {α : Type u_1} {β : Type u_2} [AddMonoidWithOne α] [AddMonoidWithOne β] (n : ℕ) [n.AtLeastTwo] :
    (OfNat.ofNat n).1 = OfNat.ofNat n
    source
    @[simp]
    theorem Prod.snd_natCast {α : Type u_1} {β : Type u_2} [AddMonoidWithOne α] [AddMonoidWithOne β] (n : ℕ) :
    (↑n).2 = ↑n
    source
    @[simp]
    theorem Prod.snd_ofNat {α : Type u_1} {β : Type u_2} [AddMonoidWithOne α] [AddMonoidWithOne β] (n : ℕ) [n.AtLeastTwo] :
    (OfNat.ofNat n).2 = OfNat.ofNat n