Commit 2024-12-20 12:30 02abf1b4

View on Github →

chore: revert import order between Algebra.Group.ZeroOne and Logic.Nonempty (#19994)

Estimated changes

Modified Mathlib/Algebra/Group/ZeroOne.lean

added theorem Subsingleton.eq_one

Modified Mathlib/CategoryTheory/Types.lean

Modified Mathlib/Data/FunLike/Basic.lean

Modified Mathlib/Data/Int/Defs.lean

Modified Mathlib/Data/Subtype.lean

Modified Mathlib/Data/TwoPointing.lean

Modified Mathlib/Logic/Equiv/Defs.lean

Modified Mathlib/Logic/Nonempty.lean

Modified Mathlib/Logic/Nontrivial/Basic.lean

deleted theorem Subsingleton.eq_one

Modified Mathlib/Order/Basic.lean

Modified Mathlib/Tactic/CategoryTheory/Reassoc.lean