OAI/GroupTheory/PolycyclicRecognition/Algebra/HyperplaneReflection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The reflection forced by agreement on a facet

  1. theorem OAI.PolycyclicRecognition.fixed_hyperplane_image_normal line 14
  2. theorem OAI.PolycyclicRecognition.orthogonal_map_fixing_hyperplane_negates_normal line 39

    Source documentation

    A nonidentity orthogonal map fixing a hyperplane reverses its normal. This is the linear step in the neighboring-label reflection argument.

    theorem orthogonal_map_fixing_hyperplane_negates_normal
    (A : W ≃ₗᵢ[ℝ] W) (v : W) (hv : v ≠ 0)
    (hfix : ∀ w, ⟪w, v⟫ = 0 → A w = w)
    (hne : A ≠ LinearIsometryEquiv.refl ℝ W) : A v = -v := by
…