Theorems · Definition · linear algebra

Module.preReflection

{R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → M → Module.Dual R M → Module.End R M

Given an element x in a module M and a linear form f on M, we define the endomorphism of M for which y ↦ y - (f y) • x. One is typically interested in this endomorphism when f x = 2; this definition exists to allow the user defer discharging this proof obligation. See also Module.reflection.

Defined in

Mathlib.LinearAlgebra.Reflection

Cited by

14 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext

Assumes

CommRingAddCommGroupModule