Commit 2024-10-19 15:25 c8922d33

View on Github →

chore: make Quotient.mk'' an abbrev of Quotient.mk _ (#16264) The plan is to deprecate Quotient.mk'' in future PRs.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Group/Finset.lean

modified theorem Finset.prod_cancels_of_partition_cancels

Modified Mathlib/Algebra/CharZero/Quotient.lean

Modified Mathlib/Data/List/Cycle.lean

Modified Mathlib/Data/Multiset/Basic.lean

Modified Mathlib/Data/Quot.lean

Modified Mathlib/Data/Set/Image.lean

modified theorem Set.Quotient.range_mk''

Modified Mathlib/GroupTheory/Coset/Basic.lean

Modified Mathlib/GroupTheory/GroupAction/Quotient.lean

Modified Mathlib/GroupTheory/PGroup.lean