mathlib
721f571a - feat(linear_algebra/basic) : add a small lemma for simplifying a map between equivalent quotient spaces (#8640)

Commit

4 years ago

feat(linear_algebra/basic) : add a small lemma for simplifying a map between equivalent quotient spaces (#8640) Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author

Paul-Lez

Parents

c765b044

mathlib 721f571a - feat(linear_algebra/basic) : add a small lemma for simplifying a map between equivalent quotient spaces (#8640)

mathlib
721f571a - feat(linear_algebra/basic) : add a small lemma for simplifying a map between equivalent quotient spaces (#8640)