Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-08 20:24 b39feab3

View on Github →

refactor(algebra/lie): reduce use of old_structure_cmd (#9616)

Estimated changes

Modified src/algebra/lie/basic.lean

added def lie_equiv.to_linear_equiv

deleted theorem lie_hom.coe_linear_mk

added def lie_hom.simps.apply

Modified src/algebra/lie/semisimple.lean

Modified src/algebra/lie/subalgebra.lean

Modified src/algebra/lie/submodule.lean