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
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