Commit 2025-03-03 23:07 fa9b3653

View on Github →

chore(Algebra/Group/Pi): separate notation from the other instances (#22499) We want to be able to recognize pointwise group operations in RefinedDiscrTree, but we don't actually need to define a full-on group structure in order to do so. So split up the notation for pi types from monoid/group/etc instances.

Estimated changes

deleted theorem Function.const_div
deleted theorem Function.const_inv
deleted theorem Function.const_mul
deleted theorem Function.const_one
deleted theorem Function.const_pow
deleted theorem Pi.comp_one
deleted theorem Pi.div_apply
deleted theorem Pi.div_comp
deleted theorem Pi.div_def
deleted theorem Pi.inv_apply
deleted theorem Pi.inv_comp
deleted theorem Pi.inv_def
deleted theorem Pi.mul_apply
deleted theorem Pi.mul_comp
deleted theorem Pi.mul_def
deleted theorem Pi.one_apply
deleted theorem Pi.one_comp
deleted theorem Pi.one_def
deleted theorem Pi.pow_apply
deleted theorem Pi.pow_comp
deleted theorem Pi.pow_def
added theorem Function.const_div
added theorem Function.const_inv
added theorem Function.const_mul
added theorem Function.const_one
added theorem Function.const_pow
added theorem Pi.comp_one
added theorem Pi.div_apply
added theorem Pi.div_comp
added theorem Pi.div_def
added theorem Pi.inv_apply
added theorem Pi.inv_comp
added theorem Pi.inv_def
added theorem Pi.mul_apply
added theorem Pi.mul_comp
added theorem Pi.mul_def
added theorem Pi.one_apply
added theorem Pi.one_comp
added theorem Pi.one_def
added theorem Pi.pow_apply
added theorem Pi.pow_comp
added theorem Pi.pow_def