Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-22 20:22 98ccc666

View on Github →

feat(algebra/lie/tensor_product): define (binary) tensor product of Lie modules (#7266)

Estimated changes

Modified src/algebra/lie/abelian.lean

added theorem lie_module.coe_maximal_trivial_linear_map_equiv_lie_module_hom

Modified src/algebra/lie/basic.lean

deleted theorem bracket_apply

added theorem lie_hom.lie_apply

added theorem lie_module_equiv.coe_mk

added theorem lie_module_hom.map_lie₂

Created src/algebra/lie/tensor_product.lean

added def tensor_product.lie_module.has_bracket_aux

added theorem tensor_product.lie_module.lie_tensor_right

added def tensor_product.lie_module.lift

added theorem tensor_product.lie_module.lift_apply

added def tensor_product.lie_module.lift_lie

added theorem tensor_product.lie_module.lift_lie_apply

Modified src/linear_algebra/tensor_product.lean

added theorem tensor_product.lift.equiv_apply

added theorem tensor_product.lift.equiv_symm_apply