theorem FiniteReflectionGroups.linearReflection_unit {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e β : E) (he : ‖e‖ = 1) : linearReflection e β = β - (2 * inner ℝ β e) • e

For a unit vector $e$, the reflection formula simplifies to $\beta - 2⟨\beta,e⟩e$.

theorem FiniteReflectionGroups.abs_inner_lt_one_of_not_parallel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e f : E) (he : ‖e‖ = 1) (hf : ‖f‖ = 1) (h_not_par : ¬∃ (c : ℝ), f = c • e) : |inner ℝ e f| < 1

Two non-parallel unit vectors have inner product of absolute value strictly less than $1$.