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