Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-01 19:11 130e07d3

View on Github →

chore(algebra/group/prod): prod.swap commutes with arithmetic (#12367) This also adds some missing div lemmas using to_additive.

Estimated changes

added theorem prod.fst_div
deleted theorem prod.fst_sub
added theorem prod.mk_div_mk
deleted theorem prod.mk_sub_mk
added theorem prod.snd_div
deleted theorem prod.snd_sub
added theorem prod.swap_div
added theorem prod.swap_inv
added theorem prod.swap_mul
added theorem prod.swap_one
added theorem prod.smul_swap