Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-15 11:28 6bc2a1a2

View on Github →

refactor(algebra/lie/basic): remove old_structure_cmd (#9721)

Estimated changes

Modified src/algebra/lie/abelian.lean

Modified src/algebra/lie/basic.lean

modified theorem lie_module_equiv.coe_mk

added theorem lie_module_equiv.injective

added def lie_module_equiv.to_equiv

added def lie_module_equiv.to_linear_equiv

modified structure lie_module_equiv

modified theorem lie_module_hom.coe_linear_mk

modified theorem lie_module_hom.coe_mk

modified theorem lie_module_hom.mk_coe

Modified src/algebra/lie/tensor_product.lean

Modified src/algebra/lie/weights.lean

added def lie_algebra.root_space_weight_space_product_aux