Commit 2023-02-27 13:06 253339bd

View on Github →

feat: port Algebra.Lie.Basic (#2262)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Lie/Basic.lean

added theorem LieEquiv.apply_symm_apply

added theorem LieEquiv.coe_injective

added theorem LieEquiv.coe_linearEquiv_injective

added theorem LieEquiv.coe_to_lieHom

added theorem LieEquiv.coe_to_linearEquiv

added theorem LieEquiv.ext

added theorem LieEquiv.one_apply

added def LieEquiv.refl

added theorem LieEquiv.refl_apply

added theorem LieEquiv.refl_symm

added theorem LieEquiv.self_trans_symm

added def LieEquiv.symm

added theorem LieEquiv.symm_apply_apply

added theorem LieEquiv.symm_symm

added theorem LieEquiv.symm_trans

added theorem LieEquiv.symm_trans_self

added def LieEquiv.toLinearEquiv

added theorem LieEquiv.to_linearEquiv_mk

added def LieEquiv.trans

added theorem LieEquiv.trans_apply

added structure LieEquiv

added def LieHom.Simps.apply

added theorem LieHom.coe_comp

added theorem LieHom.coe_id

added theorem LieHom.coe_injective

added theorem LieHom.coe_linearMap_comp

added theorem LieHom.coe_mk

added theorem LieHom.coe_one

added theorem LieHom.coe_toLinearMap

added theorem LieHom.coe_zero

added def LieHom.comp

added theorem LieHom.comp_apply

added theorem LieHom.comp_id

added theorem LieHom.congr_fun

added theorem LieHom.ext

added theorem LieHom.ext_iff

added def LieHom.id

added theorem LieHom.id_apply

added theorem LieHom.id_comp

added def LieHom.inverse

added theorem LieHom.lie_apply

added theorem LieHom.map_add

added theorem LieHom.map_lie

added theorem LieHom.map_neg

added theorem LieHom.map_smul

added theorem LieHom.map_sub

added theorem LieHom.map_zero

added theorem LieHom.mk_coe

added theorem LieHom.one_apply

added theorem LieHom.toFun_eq_coe

added theorem LieHom.zero_apply

added structure LieHom

added def LieModule.compLieHom

added theorem LieModuleEquiv.apply_symm_apply

added theorem LieModuleEquiv.coe_mk

added theorem LieModuleEquiv.coe_to_lieModuleHom

added theorem LieModuleEquiv.coe_to_linearEquiv

added theorem LieModuleEquiv.ext

added theorem LieModuleEquiv.injective

added theorem LieModuleEquiv.one_apply

added def LieModuleEquiv.refl

added theorem LieModuleEquiv.refl_apply

added theorem LieModuleEquiv.self_trans_symm

added def LieModuleEquiv.symm

added theorem LieModuleEquiv.symm_apply_apply

added theorem LieModuleEquiv.symm_symm

added theorem LieModuleEquiv.symm_trans

added theorem LieModuleEquiv.symm_trans_self

added def LieModuleEquiv.toEquiv

added theorem LieModuleEquiv.toEquiv_injective

added theorem LieModuleEquiv.toEquiv_mk

added def LieModuleEquiv.toLinearEquiv

added def LieModuleEquiv.trans

added theorem LieModuleEquiv.trans_apply

added structure LieModuleEquiv

added theorem LieModuleHom.add_apply

added theorem LieModuleHom.coe_add

added theorem LieModuleHom.coe_comp

added theorem LieModuleHom.coe_id

added theorem LieModuleHom.coe_injective

added theorem LieModuleHom.coe_linearMap_comp

added theorem LieModuleHom.coe_linear_mk

added theorem LieModuleHom.coe_mk

added theorem LieModuleHom.coe_neg

added theorem LieModuleHom.coe_nsmul

added theorem LieModuleHom.coe_smul

added theorem LieModuleHom.coe_sub

added theorem LieModuleHom.coe_to_linearMap

added theorem LieModuleHom.coe_zero

added theorem LieModuleHom.coe_zsmul

added def LieModuleHom.comp

added theorem LieModuleHom.comp_apply

added theorem LieModuleHom.congr_fun

added theorem LieModuleHom.ext

added theorem LieModuleHom.ext_iff

added def LieModuleHom.id

added theorem LieModuleHom.id_apply

added def LieModuleHom.inverse

added theorem LieModuleHom.map_add

added theorem LieModuleHom.map_lie

added theorem LieModuleHom.map_lie₂

added theorem LieModuleHom.map_neg

added theorem LieModuleHom.map_smul

added theorem LieModuleHom.map_sub

added theorem LieModuleHom.map_zero

added theorem LieModuleHom.mk_coe

added theorem LieModuleHom.neg_apply

added theorem LieModuleHom.nsmul_apply

added theorem LieModuleHom.smul_apply

added theorem LieModuleHom.sub_apply

added theorem LieModuleHom.zero_apply

added theorem LieModuleHom.zsmul_apply

added structure LieModuleHom

added def LieRingModule.compLieHom

added theorem LieRingModule.compLieHom_apply

added theorem add_lie

added theorem leibniz_lie

added theorem lie_add

added theorem lie_jacobi

added theorem lie_lie

added theorem lie_neg

added theorem lie_nsmul

added theorem lie_self

added theorem lie_skew

added theorem lie_smul

added theorem lie_sub

added theorem lie_zero

added theorem lie_zsmul

added theorem neg_lie

added theorem nsmul_lie

added theorem smul_lie

added theorem sub_lie

added theorem zero_lie

added theorem zsmul_lie