Mathlib Changelog
Changelog
About
Github
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