Mathlib v3 is deprecated. Go to Mathlib v4

Theorem module.algebra_map_End_eq_smul_id

Modification history

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