Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-14 19:54 4415dc0e

View on Github →

feat(algebra/algebra/basic): arrow_congr for alg_equiv (#5346) This is a copy of equiv.arrow_congr

Estimated changes

Modified src/algebra/algebra/basic.lean

added def alg_equiv.arrow_congr

added theorem alg_equiv.arrow_congr_comp

added theorem alg_equiv.arrow_congr_refl

added theorem alg_equiv.arrow_congr_symm

added theorem alg_equiv.arrow_congr_trans