basic): `iso.hom_congr`agrees with `linear_equiv.arrow_congr` (#13954)

Commit

3 years ago

feat(algebra/category/Module/basic): `iso.hom_congr`agrees with `linear_equiv.arrow_congr` (#13954) Co-authored-by: antoinelab01 <66086247+antoinelab01@users.noreply.github.com>

Author

antoinelab01

Parents

4f386e66

mathlib 52531532 - feat(algebra/category/Module/basic): `iso.hom_congr`agrees with `linear_equiv.arrow_congr` (#13954)

mathlib
52531532 - feat(algebra/category/Module/basic): `iso.hom_congr`agrees with `linear_equiv.arrow_congr` (#13954)