Commit 2023-06-03 15:03 bf2154ed

View on Github →

feat: port Algebra.Lie.IdealOperations (#4618)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Lie/IdealOperations.lean

added theorem LieIdeal.comap_bracket_eq

added theorem LieIdeal.comap_bracket_incl

added theorem LieIdeal.comap_bracket_incl_of_le

added theorem LieIdeal.comap_bracket_le

added theorem LieIdeal.map_bracket_eq

added theorem LieIdeal.map_bracket_le

added theorem LieIdeal.map_comap_bracket_eq

added theorem LieIdeal.map_comap_incl

added theorem LieSubmodule.bot_lie

added theorem LieSubmodule.comap_bracket_eq

added theorem LieSubmodule.comap_map_eq

added theorem LieSubmodule.inf_lie

added theorem LieSubmodule.le_comap_map

added theorem LieSubmodule.lieIdeal_oper_eq_linear_span'

added theorem LieSubmodule.lieIdeal_oper_eq_linear_span

added theorem LieSubmodule.lieIdeal_oper_eq_span

added theorem LieSubmodule.lie_bot

added theorem LieSubmodule.lie_coe_mem_lie

added theorem LieSubmodule.lie_comm

added theorem LieSubmodule.lie_eq_bot_iff

added theorem LieSubmodule.lie_inf

added theorem LieSubmodule.lie_le_iff

added theorem LieSubmodule.lie_le_inf

added theorem LieSubmodule.lie_le_left

added theorem LieSubmodule.lie_le_right

added theorem LieSubmodule.lie_mem_lie

added theorem LieSubmodule.lie_sup

added theorem LieSubmodule.map_bracket_eq

added theorem LieSubmodule.map_comap_eq

added theorem LieSubmodule.map_comap_incl

added theorem LieSubmodule.map_comap_le

added theorem LieSubmodule.mono_lie

added theorem LieSubmodule.mono_lie_left

added theorem LieSubmodule.mono_lie_right

added theorem LieSubmodule.sup_lie