Commit 2025-01-16 00:33 806f2571

View on Github →

chore: move Algebra/Group/ZeroOne/ to Data/ (#20622) Minor cleanup on the path to reducing dependencies from Data/ on other top-level directories.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Expr.lean

Modified Mathlib/Algebra/Group/Defs.lean

Modified Mathlib/Algebra/NeZero.lean

Modified Mathlib/Algebra/Order/Pi.lean

Modified Mathlib/Algebra/Order/ZeroLEOne.lean

Created Mathlib/Algebra/ZeroOne/Lemmas.lean

added theorem dite_le_one

added theorem dite_lt_one

added theorem ite_le_one

added theorem ite_lt_one

added theorem one_le_dite

added theorem one_le_ite

added theorem one_lt_dite

added theorem one_lt_ite

Modified Mathlib/Data/Num/Basic.lean

Renamed Mathlib/Algebra/Group/ZeroOne.lean to Mathlib/Data/One/Defs.lean

Modified Mathlib/Data/PNat/Defs.lean

Modified Mathlib/Data/Set/Basic.lean

Modified Mathlib/Data/Set/SymmDiff.lean

Modified Mathlib/Order/Basic.lean

deleted theorem dite_le_one

deleted theorem dite_lt_one

deleted theorem ite_le_one

deleted theorem ite_lt_one

deleted theorem one_le_dite

deleted theorem one_le_ite

deleted theorem one_lt_dite

deleted theorem one_lt_ite

Modified Mathlib/Tactic/Bound/Attribute.lean

modified def Mathlib.Tactic.Bound.declPriority

modified def Mathlib.Tactic.Bound.ineqPriority

modified def Mathlib.Tactic.Bound.scoreToConfig

modified def Mathlib.Tactic.Bound.typePriority

Modified MathlibTest/byContra.lean

Modified scripts/noshake.json