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