Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-31 09:46 43887435

View on Github →

feat(algebra/algebra/basic): add 1-related lemmas for aut (#11738) from flt-regular

Estimated changes

added theorem alg_equiv.one_apply
modified def alg_equiv.refl