The product of two add_monoid_with_one
s. #
instance
Prod.instAddMonoidWithOneProd
{α : Type u_1}
{β : Type u_2}
[inst : AddMonoidWithOne α]
[inst : AddMonoidWithOne β]
:
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