Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-05 07:41 69701295

View on Github →

chore(algebra/group/units): add a lemma about is_unit on a coerced unit (#13947)

Estimated changes