Commit 2024-05-21 19:47 c0f600fa

View on Github →

feat: define sl₂ triples and prove basic result (#13076)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Lie/Sl2.lean

added theorem IsSl2Triple.HasPrimitiveVectorWith.exists_nat

added theorem IsSl2Triple.HasPrimitiveVectorWith.lie_e_pow_succ_toEnd_f

added theorem IsSl2Triple.HasPrimitiveVectorWith.lie_f_pow_toEnd_f

added theorem IsSl2Triple.HasPrimitiveVectorWith.lie_h_pow_toEnd_f

added theorem IsSl2Triple.HasPrimitiveVectorWith.mk'

added structure IsSl2Triple.HasPrimitiveVectorWith

added theorem IsSl2Triple.e_ne_zero

added theorem IsSl2Triple.f_ne_zero

added theorem IsSl2Triple.lie_h_e_smul

added theorem IsSl2Triple.lie_lie_smul_f

added theorem IsSl2Triple.symm

added theorem IsSl2Triple.symm_iff

added structure IsSl2Triple

Modified Mathlib/Data/Nat/Order/Lemmas.lean

added theorem Nat.exists_not_and_succ_of_not_zero_of_exists

Modified Mathlib/Data/Set/Finite.lean

added theorem Set.infinite_range_iff