Documentation

Mathlib.Data.Nat.Cast.Prod

The product of two AddMonoidWithOnes. #

instance Prod.instAddMonoidWithOne {α : Type u_1} {β : Type u_2} [AddMonoidWithOne α] [AddMonoidWithOne β] :
Equations
  • Prod.instAddMonoidWithOne = let __src := Prod.instAddMonoid; let __src_1 := Prod.instOne; AddMonoidWithOne.mk
@[simp]
theorem Prod.fst_natCast {α : Type u_1} {β : Type u_2} [AddMonoidWithOne α] [AddMonoidWithOne β] (n : ) :
(n).1 = n
@[simp]
theorem Prod.fst_ofNat {α : Type u_1} {β : Type u_2} [AddMonoidWithOne α] [AddMonoidWithOne β] (n : ) [n.AtLeastTwo] :
@[simp]
theorem Prod.snd_natCast {α : Type u_1} {β : Type u_2} [AddMonoidWithOne α] [AddMonoidWithOne β] (n : ) :
(n).2 = n
@[simp]
theorem Prod.snd_ofNat {α : Type u_1} {β : Type u_2} [AddMonoidWithOne α] [AddMonoidWithOne β] (n : ) [n.AtLeastTwo] :