Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-26 15:44 9cfa33a6

View on Github →

feat(algebra/lie): implement set_like for lie_submodule (#10488) This PR provides a set_like instance for lie_submodule and uses it to define has_mem and has_le for Lie submodules / ideals.

Estimated changes