TriangularPrimary.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Primary decomposition from the triangular adjoint basis

The real triangular basis supplies the real generalized eigenspace decomposition required by the Cartan root-space construction.

theorem OAI.PolycyclicRecognition.prod_dvd_pow_card line 19

theorem OAI.PolycyclicRecognition.iSup_maxGenEigenspace_eq_top_of_annihilating_product line 31

Source documentation

An annihilating product of real linear factors gives a decomposition into generalized eigenspaces, including repeated eigenvalues.

theorem iSup_maxGenEigenspace_eq_top_of_annihilating_product
    {V : Type*} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V]
    (F : Module.End ℝ V) (S : Finset ℝ) (n : ℕ)
    (hzero : Polynomial.aeval F ((∏ a ∈ S, (Polynomial.X - Polynomial.C a)) ^ n) = 0) :
    (⨆ a : ℝ, F.maxGenEigenspace a) = ⊤ := by
…

theorem OAI.PolycyclicRecognition.TriangularAdjoint.isTriangularizable line 78
Source documentation
The real triangular adjoint basis implies real triangularizability in the generalized-eigenspace sense used by the library's Cartan theory.
```
theorem isTriangularizable (T : TriangularAdjoint L n) :
    LieModule.IsTriangularizable ℝ L L where
…
```
Mentions: OAI.PolycyclicRecognition.TriangularAdjoint