Documentation

Mathlib.Data.Nat.Cast.Prod

The product of two add_monoid_with_ones. #

instance Prod.instAddMonoidWithOneProd {α : Type u_1} {β : Type u_2} [inst : AddMonoidWithOne α] [inst : AddMonoidWithOne β] :
Equations
  • Prod.instAddMonoidWithOneProd = let src := Prod.instAddMonoidSum; let src_1 := Prod.instOneProd; AddMonoidWithOne.mk
@[simp]
theorem Prod.fst_natCast {α : Type u_1} {β : Type u_2} [inst : AddMonoidWithOne α] [inst : AddMonoidWithOne β] (n : ) :
(n).fst = n
@[simp]
theorem Prod.snd_natCast {α : Type u_2} {β : Type u_1} [inst : AddMonoidWithOne α] [inst : AddMonoidWithOne β] (n : ) :
(n).snd = n