Documentation

Mathlib.Data.Int.Cast.Prod

The product of two AddGroupWithOnes. #

instance Prod.instAddGroupWithOneProd {α : Type u_1} {β : Type u_2} [AddGroupWithOne α] [AddGroupWithOne β] :
Equations
  • Prod.instAddGroupWithOneProd = let src := Prod.instAddMonoidWithOne; let src_1 := Prod.instAddGroup; AddGroupWithOne.mk SubNegMonoid.zsmul (_ : ∀ (a : α × β), -a + a = 0)
@[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