Theorems · Definition · linear algebra

LinearMap.transvection

{R : Type u_1} →
  {V : Type u_2} →
    [inst : Semiring R] → [inst_1 : AddCommMonoid V] → [inst_2 : Module R V] → Module.Dual R V → V → V →ₗ[R] V

The transvection associated with a linear form f and a vector v. NB. In mathematics, these linear maps are only called “transvections” when f v = 0. See also Module.preReflection for a similar definition, up to a sign.

Defined in

Mathlib.LinearAlgebra.Transvection.Basic

Cited by

32 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext

Assumes

SemiringAddCommMonoidModule