Mathlib v3 is deprecated. Go to Mathlib v4

Theorem lie_algebra.special_linear.sl_non_abelian

Modification history

2021-08-26 13:06
src/algebra/lie/classical.lean
feat(*): remove the `fintype` requirement from matrices. (#8810) …
Modified lie_algebra.special_linear.sl_non_abelianView on Github →
2020-11-17 15:27
src/algebra/lie/classical.lean
refactor(algebra/lie/basic): unbundle the action in `lie_module` (#4959)
Modified lie_algebra.special_linear.sl_non_abelianView on Github →
2020-07-06 14:12
src/algebra/classical_lie_algebras.lean
refactor(*): replace nonzero with nontrivial (#3296) …
Modified lie_algebra.special_linear.sl_non_abelianView on Github →
2020-05-29 22:20
src/algebra/classical_lie_algebras.lean
chore(algebra): displace zero_ne_one_class with nonzero and make no_zero_divisors a Prop (#2847) …
Modified lie_algebra.special_linear.sl_non_abelianView on Github →
2020-05-01 15:51
src/algebra/classical_lie_algebras.lean
feat(algebra/lie_algebra): define simple Lie algebras and define classical Lie algebra, slₙ (#2567) …
Added lie_algebra.special_linear.sl_non_abelianView on Github →