Commit 2023-06-04 08:28 0353f47d

View on Github →

feat: port Algebra.Lie.TensorProduct (#4638)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Lie/TensorProduct.lean

added def LieModule.toModuleHom

added theorem LieModule.toModuleHom_apply

added theorem LieSubmodule.lieIdeal_oper_eq_tensor_map_range

added theorem TensorProduct.LieModule.coe_liftLie_eq_lift_coe

added theorem TensorProduct.LieModule.coe_linearMap_map

added def TensorProduct.LieModule.hasBracketAux

added theorem TensorProduct.LieModule.lie_tmul_right

added def TensorProduct.LieModule.lift

added def TensorProduct.LieModule.liftLie

added theorem TensorProduct.LieModule.liftLie_apply

added theorem TensorProduct.LieModule.lift_apply

added def TensorProduct.LieModule.mapIncl

added theorem TensorProduct.LieModule.mapIncl_def