Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-03 22:25 20cc59d9

View on Github →

feat(algebra/lie/basic): define missing inclusion maps (#5207)

Estimated changes

Modified src/algebra/lie/basic.lean

added def is_lie_abelian

added def lie_ideal.incl

added theorem lie_ideal.incl_apply

added theorem lie_submodule.coe_hom_of_le

added def lie_submodule.hom_of_le

added theorem lie_submodule.hom_of_le_apply

added def lie_submodule.incl

added theorem lie_submodule.incl_apply

added theorem lie_submodule.incl_eq_val

Modified src/algebra/lie/classical.lean