Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-01 08:49 2b074bea

View on Github →

feat(algebra/lie/basic): Define lattice structure for lie_submodules (#5146)

Estimated changes

Modified src/algebra/lie/basic.lean

added theorem lie_submodule.Inf_coe

added theorem lie_submodule.Inf_coe_to_submodule

added theorem lie_submodule.Inf_glb

added theorem lie_submodule.add_eq_sup

added theorem lie_submodule.bot_coe

added theorem lie_submodule.coe_injective

added theorem lie_submodule.coe_to_submodule

added theorem lie_submodule.ext

added theorem lie_submodule.le_def

added theorem lie_submodule.mem_bot

added theorem lie_submodule.mem_carrier

added theorem lie_submodule.mem_top

added theorem lie_submodule.top_coe

modified structure lie_submodule

Modified src/algebra/module/submodule.lean

added theorem submodule.mem_carrier