Commit 2025-08-07 01:38 f92ca810

View on Github →

chore(Algebra/Notation): move Pi.single earlier (#28027) The definition doesn't need anything about monoids/groups. This is useful to disentangle Finsupp results downstream.

Estimated changes

deleted theorem Pi.apply_mulSingle
deleted theorem Pi.apply_mulSingle₂
deleted def Pi.mulSingle
deleted theorem Pi.mulSingle_apply
deleted theorem Pi.mulSingle_comm
deleted theorem Pi.mulSingle_eq_of_ne'
deleted theorem Pi.mulSingle_eq_of_ne
deleted theorem Pi.mulSingle_eq_one_iff
deleted theorem Pi.mulSingle_eq_same
deleted theorem Pi.mulSingle_inj
deleted theorem Pi.mulSingle_injective
deleted theorem Pi.mulSingle_ne_one_iff
deleted theorem Pi.mulSingle_one
deleted theorem Pi.mulSingle_op
deleted theorem Pi.mulSingle_op₂
added theorem Pi.apply_mulSingle
added theorem Pi.apply_mulSingle₂
added def Pi.mulSingle
added theorem Pi.mulSingle_apply
added theorem Pi.mulSingle_comm
added theorem Pi.mulSingle_eq_of_ne'
added theorem Pi.mulSingle_eq_of_ne
added theorem Pi.mulSingle_eq_same
added theorem Pi.mulSingle_inj
added theorem Pi.mulSingle_injective
added theorem Pi.mulSingle_one
added theorem Pi.mulSingle_op
added theorem Pi.mulSingle_op₂