Theorem unique_one

Modification history

2024-10-14 13:31

Mathlib/Algebra/Group/Units/Basic.lean

chore(Algebra.Group.Units): split into `Defs` and `Basic` file (#17724) …

Modified unique_one View on Github →

2023-08-10 19:52

Mathlib/Algebra/Group/Units.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified unique_one View on Github →

2022-11-23 04:05

Mathlib/Algebra/Group/Units.lean

feat: port Algebra.Group.Units (#549) …

Added unique_one View on Github →