mathlib3
b7a7b3d9 - feat(algebra/regular): lemmas for powers of regular elements (#6356)

Commit

4 years ago

feat(algebra/regular): lemmas for powers of regular elements (#6356) Prove that an element is (left/right-)regular iff a power of it is (left/right-)regular.

Author

adomani

Parents

ec36fc06

mathlib3 b7a7b3d9 - feat(algebra/regular): lemmas for powers of regular elements (#6356)

mathlib3
b7a7b3d9 - feat(algebra/regular): lemmas for powers of regular elements (#6356)