basic): arrow_congr for alg_equiv (#5346)

Commit

5 years ago

feat(algebra/algebra/basic): arrow_congr for alg_equiv (#5346) This is a copy of equiv.arrow_congr Co-authored-by: tb65536 <tb65536@users.noreply.github.com>

Author

tb65536

Parents

07b5618a

mathlib3 4415dc0e - feat(algebra/algebra/basic): arrow_congr for alg_equiv (#5346)

mathlib3
4415dc0e - feat(algebra/algebra/basic): arrow_congr for alg_equiv (#5346)