Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-02 21:22 725fb8bc

View on Github →

feat(algebra/lie/basic): define map and comap for Lie ideals, submodules (#5181)

Estimated changes

Modified src/algebra/lie/basic.lean

added def lie_ideal.comap

added theorem lie_ideal.gc_map_comap

added def lie_ideal.map

added theorem lie_ideal.map_le_iff_le_comap

added def lie_submodule.comap

added theorem lie_submodule.gc_map_comap

added def lie_submodule.lie_span

added theorem lie_submodule.lie_span_le

added def lie_submodule.map

added theorem lie_submodule.map_le_iff_le_comap

added theorem lie_submodule.mem_lie_span

added theorem lie_submodule.subset_lie_span