English
Let x ∈ M and f ∈ Dual_R M with f x = 2. Define the endomorphism reflection h by reflection h(y) = y − f(y) x. This is the reflection map described above.
Русский
Пусть x ∈ M и f ∈ Dual_R M удовлетворяют f x = 2. Определим отображение reflection h: M → M заданное reflection(h)(y) = y − f(y) x. Это и есть описанное выше отражение.
LaTeX
$$$\\text{Let }R,M,\\text{ and }x,f\\text{ satisfy }f(x)=2.\\n\\text{Then } reflection(h):M\\to M\\text{ is given by } reflection(h)(y)=y-f(y)\\,x.$$$
Lean4
/-- Given an element `x` in a module `M` and a linear form `f` on `M` for which `f x = 2`, we define
the endomorphism of `M` for which `y ↦ y - (f y) • x`.
It is an involutive endomorphism of `M` fixing the kernel of `f` for which `x ↦ -x`. -/
def reflection (h : f x = 2) : M ≃ₗ[R] M :=
{ preReflection x f, (involutive_preReflection h).toPerm with }
