Commit 2024-04-21 16:33 01ce6da3

View on Github →

chore: Rename a few lemmas about Pi.mulSingle (#12317) Before this PR, the MonoidHom version of Pi.mulSingle was called MonoidHom.single for brevity; but this is confusing when contrasted with MulHom.single which is about Pi.single. After this PR, the name is MonoidHom.mulSingle. Also fix the name of Pi.single_div since it is about Pi.mulSingle (and we don't have the lemma that would be called Pi.single_div).

Estimated changes

Modified Mathlib/Algebra/BigOperators/Pi.lean

Modified Mathlib/Algebra/Group/Pi/Lemmas.lean

added def MonoidHom.mulSingle

added theorem MonoidHom.mulSingle_apply

deleted def MonoidHom.single

deleted theorem MonoidHom.single_apply

added theorem OneHom.mulSingle_apply

deleted def OneHom.single

deleted theorem OneHom.single_apply

added theorem Pi.mulSingle_div

deleted theorem Pi.single_div

Modified Mathlib/Data/Finset/NoncommProd.lean

Modified Mathlib/GroupTheory/NoncommPiCoprod.lean

Modified Mathlib/GroupTheory/Subgroup/Basic.lean

Modified Mathlib/GroupTheory/Subgroup/Finite.lean

Modified Mathlib/Probability/Moments.lean

Modified Mathlib/RingTheory/PiTensorProduct.lean