Mathlib v3 is deprecated. Go to Mathlib v4

Theorem module.ker_algebra_map_End

Modification history

2020-10-23 05:47
src/algebra/algebra/basic.lean
refactor(*): lmul is an algebra hom (#4724) …
Modified module.ker_algebra_map_EndView on Github →
2020-08-28 16:07
src/ring_theory/algebra.lean
feat(linear_algebra): eigenspaces of linear maps (#3927) …
Added module.ker_algebra_map_EndView on Github →