units): If `z * w = 1`, then `z = w` (#18499)

Commit

2 years ago

feat(data/int/units): If `z * w = 1`, then `z = w` (#18499) This PR adds a lemma stating that if `z * w = 1`, then `z = w`. mathlib4 PR: https://github.com/leanprover-community/mathlib4/pull/2497

Author

tb65536

Parents

ea94d7cd

mathlib 45a1ada0 - feat(data/int/units): If `z * w = 1`, then `z = w` (#18499)

mathlib
45a1ada0 - feat(data/int/units): If `z * w = 1`, then `z = w` (#18499)