mathlib
91cc3f06 - feat(linear_algebra/basic): ker of a linear map equals ker of the corresponding group hom (#13858)

Commit

3 years ago

feat(linear_algebra/basic): ker of a linear map equals ker of the corresponding group hom (#13858) Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author

ADedecker

Parents

c12536a7

mathlib 91cc3f06 - feat(linear_algebra/basic): ker of a linear map equals ker of the corresponding group hom (#13858)

mathlib
91cc3f06 - feat(linear_algebra/basic): ker of a linear map equals ker of the corresponding group hom (#13858)