Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-14 23:07 dc719a9d

View on Github →

feat(algebra/lie/basic): define ideal operations for Lie modules (#5337)

Estimated changes

Modified src/algebra/lie/basic.lean

added def derived_lie_ideal

added def derived_lie_submodule

modified theorem lie_submodule.add_eq_sup

added theorem lie_submodule.bot_lie

added theorem lie_submodule.coe_submodule_le_coe_submodule

added theorem lie_submodule.coe_sup

added theorem lie_submodule.coe_to_set_mk

added theorem lie_submodule.coe_to_submodule_mk

added theorem lie_submodule.eq_bot_iff

modified theorem lie_submodule.le_def

added theorem lie_submodule.lie_bot

added theorem lie_submodule.lie_comm

added theorem lie_submodule.lie_ideal_oper_eq_span

added theorem lie_submodule.lie_le_inf

added theorem lie_submodule.lie_le_left

added theorem lie_submodule.lie_le_right

added theorem lie_submodule.lie_mem_lie

added theorem lie_submodule.lie_sup

added theorem lie_submodule.mem_sup

added theorem lie_submodule.mono_lie

added theorem lie_submodule.mono_lie_left

added theorem lie_submodule.mono_lie_right

added theorem lie_submodule.sup_lie

added theorem trivial_iff_derived_eq_bot

Modified src/algebra/module/submodule.lean

added theorem submodule.mk_coe

Modified src/linear_algebra/finite_dimensional.lean