Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-14 11:02 15fcb8a1

View on Github →

feat(algebra/lie_algebra): define equivalences, direct sums of Lie algebras (#2404) This pull request does two things:

Defines equivalences of Lie algebras (and proves that these do indeed form an equivalence relation)
Defines direct sums of Lie algebras The intention is to knock another chip off https://github.com/leanprover-community/mathlib/issues/1093

Estimated changes

Modified src/algebra/lie_algebra.lean

added theorem lie_algebra.direct_sum.bracket_apply

added def lie_algebra.equiv.refl

added def lie_algebra.equiv.symm

added def lie_algebra.equiv.trans

added structure lie_algebra.equiv

modified theorem lie_algebra.map_lie'

modified theorem lie_algebra.map_lie

added def lie_algebra.morphism.comp

added theorem lie_algebra.morphism.comp_apply

added def lie_algebra.morphism.inverse

modified structure lie_algebra.morphism