nilpotent): a non-trivial nilpotent Lie module has non-trivial maximal trivial submodule (#11515)

Commit

3 years ago

feat(algebra/lie/nilpotent): a non-trivial nilpotent Lie module has non-trivial maximal trivial submodule (#11515) The main result is `lie_module.nontrivial_max_triv_of_is_nilpotent`

Author

ocfnash

Parents

a0da4f1f

mathlib 5bbc187e - feat(algebra/lie/nilpotent): a non-trivial nilpotent Lie module has non-trivial maximal trivial submodule (#11515)

mathlib
5bbc187e - feat(algebra/lie/nilpotent): a non-trivial nilpotent Lie module has non-trivial maximal trivial submodule (#11515)