Documentation

Mathlib.Data.Int.Cast.Prod

The product of two AddGroupWithOnes. #

source
@[instance_reducible]
instance Prod.instAddGroupWithOne {α : Type u_1} {β : Type u_2} [AddGroupWithOne α] [AddGroupWithOne β] :
AddGroupWithOne (α × β)
Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem Prod.fst_intCast {α : Type u_1} {β : Type u_2} [AddGroupWithOne α] [AddGroupWithOne β] (n : ℤ) :
(↑n).1 = ↑n
source
@[simp]
theorem Prod.snd_intCast {α : Type u_1} {β : Type u_2} [AddGroupWithOne α] [AddGroupWithOne β] (n : ℤ) :
(↑n).2 = ↑n