Mathlib Changelog
v4
Changelog
About
Github
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