Commit 2023-06-03 07:32 00687379

View on Github →

feat: port Algebra.Lie.OfAssociative (#4617)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Lie/OfAssociative.lean

added def AlgEquiv.toLieEquiv

added theorem AlgEquiv.toLieEquiv_apply

added theorem AlgEquiv.toLieEquiv_symm_apply

added theorem AlgHom.coe_to_lieHom

added def AlgHom.toLieHom

added theorem AlgHom.toLieHom_apply

added theorem AlgHom.to_lieHom_comp

added theorem AlgHom.to_lieHom_id

added theorem AlgHom.to_lieHom_injective

added theorem Commute.lie_eq

added def LieAlgebra.ad

added theorem LieAlgebra.ad_apply

added theorem LieAlgebra.ad_eq_lmul_left_sub_lmul_right

added def LieModule.ofAssociativeModule

added def LieModule.toEndomorphism

added theorem LieModule.toEndomorphism_module_end

added theorem LieRing.lie_apply

added theorem LieRing.of_associative_ring_bracket

added def LieRingModule.ofAssociativeModule

added theorem LieSubalgebra.ad_comp_incl_eq

added theorem LieSubalgebra.toEndomorphism_eq

added theorem LieSubalgebra.toEndomorphism_mk

added theorem LieSubmodule.coe_map_toEndomorphism_le

added theorem LieSubmodule.toEndomorphism_comp_subtype_mem

added theorem LieSubmodule.toEndomorphism_restrict_eq_toEndomorphism

added def LinearEquiv.lieConj

added theorem LinearEquiv.lieConj_apply

added theorem LinearEquiv.lieConj_symm

added theorem Ring.lie_def

added theorem commute_iff_lie_eq

added def lieSubalgebraOfSubalgebra

added theorem lie_eq_smul