Commit 2023-03-22 13:29 9735f787

View on Github →

feat: port Algebra.Lie.Subalgebra (#3016)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Lie/Subalgebra.lean

added def LieEquiv.lieSubalgebraMap

added theorem LieEquiv.lieSubalgebraMap_apply

added def LieEquiv.ofEq

added theorem LieEquiv.ofEq_apply

added theorem LieEquiv.ofInjective_apply

added def LieEquiv.ofSubalgebras

added theorem LieEquiv.ofSubalgebras_apply

added theorem LieEquiv.ofSubalgebras_symm_apply

added theorem LieHom.equivRangeOfInjective_apply

added theorem LieHom.mem_range

added theorem LieHom.mem_range_self

added def LieHom.range

added def LieHom.rangeRestrict

added theorem LieHom.rangeRestrict_apply

added theorem LieHom.range_coe

added theorem LieHom.range_eq_map

added theorem LieHom.surjective_rangeRestrict

added theorem LieModuleHom.coe_restrictLie

added def LieModuleHom.restrictLie

added theorem LieSubalgebra.add_eq_sup

added theorem LieSubalgebra.bot_coe

added theorem LieSubalgebra.bot_coe_submodule

added theorem LieSubalgebra.coe_bracket

added theorem LieSubalgebra.coe_bracket_of_module

added theorem LieSubalgebra.coe_homOfLe

added theorem LieSubalgebra.coe_incl'

added theorem LieSubalgebra.coe_incl

added theorem LieSubalgebra.coe_injective

added theorem LieSubalgebra.coe_lieSpan_submodule_eq_iff

added theorem LieSubalgebra.coe_ofLe

added theorem LieSubalgebra.coe_set_eq

added theorem LieSubalgebra.coe_submodule_le_coe_submodule

added theorem LieSubalgebra.coe_to_submodule

added theorem LieSubalgebra.coe_to_submodule_eq_iff

added theorem LieSubalgebra.coe_to_submodule_mk

added theorem LieSubalgebra.coe_zero_iff_zero

added def LieSubalgebra.comap

added theorem LieSubalgebra.eq_bot_iff

added theorem LieSubalgebra.equivOfLe_apply

added theorem LieSubalgebra.ext

added theorem LieSubalgebra.ext_iff'

added theorem LieSubalgebra.ext_iff

added theorem LieSubalgebra.gc_map_comap

added def LieSubalgebra.homOfLe

added theorem LieSubalgebra.homOfLe_apply

added theorem LieSubalgebra.homOfLe_injective

added def LieSubalgebra.incl'

added def LieSubalgebra.incl

added theorem LieSubalgebra.incl_range

added theorem LieSubalgebra.inf_coe

added theorem LieSubalgebra.inf_coe_to_submodule

added theorem LieSubalgebra.infₛ_coe

added theorem LieSubalgebra.infₛ_coe_to_submodule

added theorem LieSubalgebra.infₛ_glb

added theorem LieSubalgebra.le_def

added def LieSubalgebra.lieSpan

added theorem LieSubalgebra.lieSpan_eq

added theorem LieSubalgebra.lieSpan_le

added theorem LieSubalgebra.lieSpan_mono

added theorem LieSubalgebra.lie_mem

added def LieSubalgebra.map

added theorem LieSubalgebra.map_le_iff_le_comap

added theorem LieSubalgebra.mem_bot

added theorem LieSubalgebra.mem_carrier

added theorem LieSubalgebra.mem_coe

added theorem LieSubalgebra.mem_coe_submodule

added theorem LieSubalgebra.mem_inf

added theorem LieSubalgebra.mem_lieSpan

added theorem LieSubalgebra.mem_map

added theorem LieSubalgebra.mem_map_submodule

added theorem LieSubalgebra.mem_mk_iff

added theorem LieSubalgebra.mem_ofLe

added theorem LieSubalgebra.mem_top

added theorem LieSubalgebra.mk_coe

added def LieSubalgebra.ofLe

added theorem LieSubalgebra.ofLe_eq_comap_incl

added theorem LieSubalgebra.smul_mem

added theorem LieSubalgebra.span_empty

added theorem LieSubalgebra.span_union

added theorem LieSubalgebra.span_unionᵢ

added theorem LieSubalgebra.span_univ

added theorem LieSubalgebra.submodule_span_le_lieSpan

added theorem LieSubalgebra.subset_lieSpan

added theorem LieSubalgebra.subsingleton_bot

added theorem LieSubalgebra.to_submodule_injective

added theorem LieSubalgebra.top_coe

added theorem LieSubalgebra.top_coe_submodule

added theorem LieSubalgebra.wellFounded_of_noetherian

added structure LieSubalgebra

added theorem Submodule.exists_lieSubalgebra_coe_eq_iff