mathlib
2ef444af - feat(linear_algebra/basic): range of `linear_map.prod` (#2785)

Commit

5 years ago

feat(linear_algebra/basic): range of `linear_map.prod` (#2785) Also make `ker_prod` a `simp` lemma. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author

urkud

Parents

5449203f

mathlib 2ef444af - feat(linear_algebra/basic): range of `linear_map.prod` (#2785)

mathlib
2ef444af - feat(linear_algebra/basic): range of `linear_map.prod` (#2785)