Commit 2024-09-02 17:50 404524a3

View on Github →

chore: move Init.Data.Quot to Logic.Relation (#16378)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/RingQuot.lean

modified theorem RingQuot.eqvGen_rel_eq

Modified Mathlib/CategoryTheory/Groupoid/FreeGroupoid.lean

Modified Mathlib/CategoryTheory/Limits/Final.lean

Modified Mathlib/CategoryTheory/Limits/IsConnected.lean

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

Modified Mathlib/CategoryTheory/Limits/Types.lean

Modified Mathlib/CategoryTheory/Limits/TypesFiltered.lean

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

Modified Mathlib/Data/Quot.lean

Modified Mathlib/Data/Setoid/Basic.lean

modified theorem Quot.subsingleton_iff

modified theorem Setoid.eqvGen_idem

modified theorem Setoid.eqvGen_of_setoid

modified def Setoid.gi

modified theorem Setoid.sSup_def

modified theorem Setoid.sup_def

Modified Mathlib/FieldTheory/PerfectClosure.lean

Modified Mathlib/GroupTheory/FreeGroup/Basic.lean

Deleted Mathlib/Init/Data/Quot.lean

deleted def EqvGen.Setoid

deleted theorem EqvGen.is_equivalence

deleted inductive EqvGen

deleted theorem Quot.eqvGen_exact

deleted theorem Quot.eqvGen_sound

Modified Mathlib/Logic/Relation.lean

deleted theorem EqvGen.mono

added theorem Quot.eqvGen_exact

added theorem Quot.eqvGen_sound

added theorem Relation.EqvGen.is_equivalence

added theorem Relation.EqvGen.mono

added def Relation.EqvGen.setoid

added inductive Relation.EqvGen

Modified Mathlib/Topology/Gluing.lean