Commit 2025-03-10 06:24 7bc8f159

View on Github →

chore(Algebra/Group/Prod): move notation to a new file (#22567)

Estimated changes

deleted theorem Prod.pow_def
deleted theorem Prod.pow_fst
deleted theorem Prod.pow_mk
deleted theorem Prod.pow_snd
deleted theorem Prod.pow_swap
deleted theorem Prod.smul_def
deleted theorem Prod.smul_fst
deleted theorem Prod.smul_mk
deleted theorem Prod.smul_snd
deleted theorem Prod.smul_swap
deleted theorem Prod.div_def
deleted theorem Prod.fst_div
deleted theorem Prod.fst_inv
deleted theorem Prod.fst_mul
deleted theorem Prod.inv_mk
deleted theorem Prod.mk_div_mk
deleted theorem Prod.mk_mul_mk
modified theorem Prod.mk_one_mul_mk_one
deleted theorem Prod.mul_def
modified theorem Prod.one_mk_mul_one_mk
deleted theorem Prod.snd_div
deleted theorem Prod.snd_inv
deleted theorem Prod.snd_mul
deleted theorem Prod.swap_div
deleted theorem Prod.swap_inv
deleted theorem Prod.swap_mul
added theorem Prod.div_def
added theorem Prod.fst_div
added theorem Prod.fst_inv
added theorem Prod.fst_mul
modified theorem Prod.fst_one
added theorem Prod.inv_mk
added theorem Prod.mk_div_mk
modified theorem Prod.mk_eq_one
added theorem Prod.mk_mul_mk
modified theorem Prod.mk_one_one
added theorem Prod.mul_def
modified theorem Prod.one_eq_mk
added theorem Prod.pow_def
added theorem Prod.pow_fst
added theorem Prod.pow_mk
added theorem Prod.pow_snd
added theorem Prod.pow_swap
added theorem Prod.smul_def
added theorem Prod.smul_fst
added theorem Prod.smul_mk
added theorem Prod.smul_snd
added theorem Prod.smul_swap
added theorem Prod.snd_div
added theorem Prod.snd_inv
added theorem Prod.snd_mul
modified theorem Prod.snd_one
added theorem Prod.swap_div
added theorem Prod.swap_inv
added theorem Prod.swap_mul
modified theorem Prod.swap_one