Commit 2024-07-16 11:03 e29855b5

View on Github →

chore(Data/Int/Defs): clear out Init/Data/Int/Basic (#14759)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Defs.lean

Renamed Mathlib/Init/Data/Int/Basic.lean to Mathlib/Data/Int/Align.lean

deleted def Int.natMod

Modified Mathlib/Data/Int/Defs.lean

added def Int.natMod

Created Mathlib/Data/Int/Notation.lean

Modified Mathlib/Data/Num/Basic.lean

Modified Mathlib/Init/Data/Int/Order.lean

Modified Mathlib/Logic/Basic.lean

Modified Mathlib/Tactic/Lift.lean

Modified scripts/noshake.json