Commit 2023-01-23 17:36 755274ff

View on Github →

feat: port Data.ZMod.Defs (#1713)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Fintype/Basic.lean

Modified Mathlib/Data/Fintype/Card.lean

Modified Mathlib/Data/UInt.lean

Created Mathlib/Data/ZMod/Defs.lean

added theorem ZMod.card

added def ZMod

Deleted Mathlib/Data/Zmod/AdHocDefs.lean

deleted def Fin.ofInt'

Modified Mathlib/Logic/Basic.lean

Modified scripts/start_port.sh

Modified scripts/style-exceptions.txt