OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanNontrivialHeight.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Nontrivial height forces the nonzero sampling branch

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.nonempty_letters_of_nontrivial_height line 22

    Source documentation

    With no generator weights, separation makes the height space trivial.

    theorem nonempty_letters_of_nontrivial_height [Nontrivial W] :
    Nonempty (Fin M.letterCount) := by
…
  2. theorem OAI.PolycyclicRecognition.CartanWordModel.nonempty_root_coordinates_of_nonempty_letters line 31

    Source documentation

    A retained generator gives positive dimension of the root ideal.

    theorem nonempty_root_coordinates_of_nonempty_letters
    [Nonempty (Fin M.letterCount)] :
    Nonempty (Fin (finrank ℝ (cartanRootIdeal H))) := by
…

    Mentions: OAI.PolycyclicRecognition.cartanRootIdeal