Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-15 14:40 c347c75d

View on Github →

feat(algebra/lie/basic): add a few simp lemmas (#5757)

Estimated changes

Modified src/algebra/lie/basic.lean

added theorem coe_to_subalgebra

added theorem lie_algebra.morphism.map_add

added theorem lie_algebra.morphism.map_smul

modified def lie_algebra.morphism.range

modified theorem lie_algebra.morphism.range_bracket

added theorem lie_algebra.morphism.range_coe

modified def lie_subalgebra.map

added theorem lie_submodule.bot_coe_submodule

deleted theorem lie_submodule.coe_sup

added theorem lie_submodule.coe_to_submodule_eq_iff

added theorem lie_submodule.inf_coe

added theorem lie_submodule.inf_coe_to_submodule

added theorem lie_submodule.inf_lie

added theorem lie_submodule.lie_inf

added theorem lie_submodule.lie_span_eq

added theorem lie_submodule.mem_inf

added theorem lie_submodule.sup_coe_to_submodule

added theorem lie_submodule.top_coe_submodule