Commit 2024-08-26 15:01 9b51ed22

View on Github →

chore: delete Init.Quot (#16149)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Fintype/Card.lean

Modified Mathlib/Data/List/Cycle.lean

Modified Mathlib/Data/Multiset/Basic.lean

Modified Mathlib/Data/Quot.lean

Deleted Mathlib/Init/Quot.lean

deleted theorem Quotient.mk'_eq_mk

Modified Mathlib/Logic/Equiv/List.lean