The product of two add_monoid_with_ones. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[protected, instance]
def
prod.add_monoid_with_one
{α : Type u_1}
{β : Type u_2}
[add_monoid_with_one α]
[add_monoid_with_one β] :
add_monoid_with_one (α × β)
Equations
- prod.add_monoid_with_one = {nat_cast := λ (n : ℕ), (↑n, ↑n), add := add_monoid.add prod.add_monoid, add_assoc := _, zero := add_monoid.zero prod.add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul prod.add_monoid, nsmul_zero' := _, nsmul_succ' := _, one := 1, nat_cast_zero := _, nat_cast_succ := _}
@[simp]
theorem
prod.fst_nat_cast
{α : Type u_1}
{β : Type u_2}
[add_monoid_with_one α]
[add_monoid_with_one β]
(n : ℕ) :
@[simp]
theorem
prod.snd_nat_cast
{α : Type u_1}
{β : Type u_2}
[add_monoid_with_one α]
[add_monoid_with_one β]
(n : ℕ) :