mathlib3 documentation

data.int.cast.prod

The product of two add_group_with_ones. #

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

@[simp]
theorem prod.fst_int_cast {α : Type u_1} {β : Type u_2} [add_group_with_one α] [add_group_with_one β] (n : ) :
@[simp]
theorem prod.snd_int_cast {α : Type u_1} {β : Type u_2} [add_group_with_one α] [add_group_with_one β] (n : ) :