OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanConeInvariance.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual Cartan automorphisms preserve the cone ideal

  1. theorem OAI.PolycyclicRecognition.map_mixedWordIdeal_mem line 13
  2. theorem OAI.PolycyclicRecognition.mem_submodule_equiv_iff_of_invariant line 32

    Source documentation

    In finite dimension an invariant subspace is also invariant under the inverse automorphism.

    theorem mem_submodule_equiv_iff_of_invariant
    {V : Type*} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V]
    (J : Submodule ℝ V) (e : V ≃ₗ[ℝ] V) (he : ∀ v ∈ J, e v ∈ J) (v : V) :
    e v ∈ J ↔ v ∈ J := by
…
  3. theorem OAI.PolycyclicRecognition.CartanWordModel.coneWordIdeal_adjoint_mem line 50
  4. theorem OAI.PolycyclicRecognition.CartanWordModel.coneWordIdeal_adjoint_mem_iff line 72