Commit 2023-03-19 19:01 2fda1839

View on Github →

feat: forward-port leanprover-community/mathlib#18359 (#2106) Also fixes a lemma statement to use % notation like it did in Lean3

Estimated changes

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

Modified Mathlib/Data/Nat/Basic.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Basic.lean

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

modified def Int.natMod

Modified Mathlib/Logic/Equiv/Fin.lean

added def Int.divModEquiv

added def Nat.divModEquiv