The product of two AddGroupWithOnes. #
instance
Prod.instAddGroupWithOne
{α : Type u_1}
{β : Type u_2}
[AddGroupWithOne α]
[AddGroupWithOne β]
:
AddGroupWithOne (α × β)
Equations
- Prod.instAddGroupWithOne = AddGroupWithOne.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
@[simp]
theorem
Prod.fst_intCast
{α : Type u_1}
{β : Type u_2}
[AddGroupWithOne α]
[AddGroupWithOne β]
(n : ℤ)
:
(↑n).1 = ↑n
@[simp]
theorem
Prod.snd_intCast
{α : Type u_1}
{β : Type u_2}
[AddGroupWithOne α]
[AddGroupWithOne β]
(n : ℤ)
:
(↑n).2 = ↑n