Mathlib v3 is deprecated. Go to Mathlib v4

Def is_right_regular

Modification history

2022-08-31 08:44

src/algebra/regular/basic.lean

chore(algebra/regular/basic): clean up variables and slight golf (#16321) …

Modified is_right_regular View on Github →

2021-02-20 17:42

src/algebra/regular.lean

feat(algebra/regular): define regular elements (#6282) …

Added is_right_regular View on Github →