mathlib3 documentation

data.nat.cast.prod

The product of two add_monoid_with_ones. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[simp]
theorem prod.fst_nat_cast {α : Type u_1} {β : Type u_2} [add_monoid_with_one α] [add_monoid_with_one β] (n : ) :
@[simp]
theorem prod.snd_nat_cast {α : Type u_1} {β : Type u_2} [add_monoid_with_one α] [add_monoid_with_one β] (n : ) :