Theorem Nat.units_eq_one

Modification history

2024-11-22 21:24

Mathlib/Algebra/Group/Nat/Even.lean

chore: split Algebra.Group.Nat (#19375)

Modified Nat.units_eq_one View on Github →

2024-05-15 20:27

Mathlib/Algebra/Group/Nat.lean

chore: Delete `Data.Nat.Units`, `Data.Int.Units` (#12835) …

Modified Nat.units_eq_one View on Github →

2022-11-30 20:46

Mathlib/Data/Nat/Units.lean

feat: port Data.Nat.Units (#805) …

Added Nat.units_eq_one View on Github →