Commit 2023-06-08 08:38 84610768

View on Github →

feat: port Algebra.Lie.Normalizer (#4843)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Lie/Normalizer.lean

added theorem LieSubalgebra.coe_normalizer_eq_normalizer

added theorem LieSubalgebra.exists_nested_lieIdeal_ofLe_normalizer

added theorem LieSubalgebra.ideal_in_normalizer

added theorem LieSubalgebra.le_normalizer

added theorem LieSubalgebra.lie_mem_sup_of_mem_normalizer

added theorem LieSubalgebra.mem_normalizer_iff'

added theorem LieSubalgebra.mem_normalizer_iff

added def LieSubalgebra.normalizer

added theorem LieSubalgebra.normalizer_eq_self_iff

added theorem LieSubmodule.comap_normalizer

added theorem LieSubmodule.gc_top_lie_normalizer

added theorem LieSubmodule.le_normalizer

added theorem LieSubmodule.mem_normalizer

added theorem LieSubmodule.monotone_normalizer

added def LieSubmodule.normalizer

added theorem LieSubmodule.normalizer_bot_eq_maxTrivSubmodule

added theorem LieSubmodule.normalizer_inf

added theorem LieSubmodule.top_lie_le_iff_le_normalizer