OAI/GroupTheory/PolycyclicRecognition/Algebra/PositiveRayPullback.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.outside_ray_of_surjective_pullback line 12

   Source documentation

   If a target ray pulls back to a positive multiple of a source generator weight, every other target ray has a quotient that kills that generator.

   theorem outside_ray_of_surjective_pullback
       {V W : Type*} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W]
       (θ : V →ₗ[ℝ] W) (hθ : Function.Surjective θ)
       (α γ : W →ₗ[ℝ] ℝ) (β : V →ₗ[ℝ] ℝ)
       {t : ℝ} (ht : 0 < t) (hmatch : α.comp θ = t • β)
       (hout : γ ∉ positiveWeightRay α) : β ∉ positiveWeightRay (γ.comp θ) := by
   …

   Mentions: OAI.PolycyclicRecognition.positiveWeightRay