The product of two AddMonoidWithOnes.

@[instance_reducible]

instance Prod.instAddMonoidWithOne {α : Type u_1} {β : Type u_2} [AddMonoidWithOne α] [AddMonoidWithOne β] : AddMonoidWithOne (α × β)

Equations

• Prod.instAddMonoidWithOne = { natCast := fun (n : ℕ) => (↑n, ↑n), toAddMonoid := Prod.instAddMonoid, toOne := Prod.instOne, natCast_zero := ⋯, natCast_succ := ⋯ }

@[simp]

theorem Prod.fst_natCast {α : Type u_1} {β : Type u_2} [AddMonoidWithOne α] [AddMonoidWithOne β] (n : ℕ) : (↑n).1 = ↑n

@[simp]

theorem Prod.fst_ofNat {α : Type u_1} {β : Type u_2} [AddMonoidWithOne α] [AddMonoidWithOne β] (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).1 = OfNat.ofNat n

@[simp]

theorem Prod.snd_natCast {α : Type u_1} {β : Type u_2} [AddMonoidWithOne α] [AddMonoidWithOne β] (n : ℕ) : (↑n).2 = ↑n

@[simp]

theorem Prod.snd_ofNat {α : Type u_1} {β : Type u_2} [AddMonoidWithOne α] [AddMonoidWithOne β] (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).2 = OfNat.ofNat n