mathlib
d2db3e83 - chore(algebra/lie_algebra): add function coercion for morphisms (#2434)

Commit
5 years ago
chore(algebra/lie_algebra): add function coercion for morphisms (#2434) In fact three different changes are being made here: 1. Adding direct function coercion for `lie_algebra.morphism`, allowing us to tidy up `map_lie` and increase simp scope 2. Providing a zero element for `lie_subalgebra`, thus allowing removal of a `has_inhabited_instance` exception in nolints.txt 3. Providing a zero element for `lie_submodule`, thus allowing removal of a `has_inhabited_instance` exception in nolints.txt
Author
Oliver Nash
Parents
Loading