reflection_smul — Mathlib

English

Applying a reflection automorphism to a vector is the same as applying the corresponding linear map to the vector.

Русский

Применение отражательного автоморфизма к вектору равно применению соответствующей линейной карты к вектору.

LaTeX

$$$\\\\text{reflection}(P,i) \\cdot x = P.reflection i (x).$$$

Lean4

@[simp]
theorem reflection_smul (i : ι) (x : M) : Equiv.reflection P i • x = P.reflection i x :=
  rfl

Похожие утверждения