Commit 2023-01-20 01:16 b163ce83

View on Github →

feat: port Data.Fintype.Units (#1696)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Fintype/Units.lean

added theorem Fintype.card_units

added theorem Fintype.card_units_int

added theorem UnitsInt.univ