The product of two add_group_with_ones. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[protected, instance]
def
prod.add_group_with_one
{α : Type u_1}
{β : Type u_2}
[add_group_with_one α]
[add_group_with_one β] :
add_group_with_one (α × β)
Equations
- prod.add_group_with_one = {int_cast := λ (n : ℤ), (↑n, ↑n), add := add_monoid_with_one.add prod.add_monoid_with_one, add_assoc := _, zero := add_monoid_with_one.zero prod.add_monoid_with_one, zero_add := _, add_zero := _, nsmul := add_monoid_with_one.nsmul prod.add_monoid_with_one, nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg prod.add_group, sub := add_group.sub prod.add_group, sub_eq_add_neg := _, zsmul := add_group.zsmul prod.add_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, nat_cast := add_monoid_with_one.nat_cast prod.add_monoid_with_one, one := add_monoid_with_one.one prod.add_monoid_with_one, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _}
@[simp]
theorem
prod.fst_int_cast
{α : Type u_1}
{β : Type u_2}
[add_group_with_one α]
[add_group_with_one β]
(n : ℤ) :
@[simp]
theorem
prod.snd_int_cast
{α : Type u_1}
{β : Type u_2}
[add_group_with_one α]
[add_group_with_one β]
(n : ℤ) :