Commit 2024-08-31 18:37 2b3a9f77

View on Github →

chore(Init/Data/Quot): better naming (#16252) Quot.exact ↦ Quot.eqvGen_exact Quot.EqvGen_sound ↦ Quot.eqvGen_sound

Estimated changes

Modified Mathlib/Algebra/Category/Grp/FilteredColimits.lean

Modified Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean

Modified Mathlib/Algebra/Category/MonCat/FilteredColimits.lean

Modified Mathlib/CategoryTheory/Groupoid/FreeGroupoid.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Types.lean

Modified Mathlib/Data/PFunctor/Multivariate/M.lean

Modified Mathlib/Data/Quot.lean

Modified Mathlib/FieldTheory/PerfectClosure.lean

Modified Mathlib/GroupTheory/FreeGroup/Basic.lean

Modified Mathlib/Init/Data/Quot.lean

deleted theorem Quot.EqvGen_sound

added theorem Quot.eqvGen_exact

added theorem Quot.eqvGen_sound

deleted theorem Quot.exact