Theorems · Definition · linear algebra

Module.reflection

{R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {x : M} → {f : Module.Dual R M} → f x = 2 → M ≃ₗ[R] M

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.

Defined in

Mathlib.LinearAlgebra.Reflection

Cited by

25 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModule