mathlib

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

chore(algebra/regular/basic): clean up variables and slight golf (#16321) Re-organize variables in the file, so that typeclass assumptions appear earlier. Also, golf two proofs and remove two unneeded `@`.