Commit 2023-03-06 17:29 0ecf8c35

View on Github →

feat(Data/Int/Units): If z * w = 1, then z = w (#2497) This PR adds a lemma stating that if z * w = 1, then z = w. mathlib PR: https://github.com/leanprover-community/mathlib/pull/18499

Estimated changes