Commit 2024-03-13 10:15 9fb3e1ad

View on Github →

feat(Algebra/Ring/Equiv): add lemma isUnit_iff (#11237) Add one lemma stating that an element is a unit if and only if its image through a ring equivalence is a unit.

Estimated changes