Commit 2024-05-27 04:51 55e0f3e6

View on Github →

feat(Algebra/Lie/Sl2): Two lemmas for the action of sl2 triples. (#13259)

Estimated changes

Modified Mathlib/Algebra/Lie/Sl2.lean

modified theorem IsSl2Triple.HasPrimitiveVectorWith.lie_f_pow_toEnd_f

added theorem IsSl2Triple.HasPrimitiveVectorWith.pow_toEnd_f_eq_zero_of_eq_nat

added theorem IsSl2Triple.HasPrimitiveVectorWith.pow_toEnd_f_ne_zero_of_eq_nat