Theorems · Definition · number theory

QuadraticMap.polar

{M : Type u_4} → {N : Type u_5} → [AddCommGroup M] → [AddCommGroup N] → (M → N) → M → M → N

Up to a factor 2, Q.polar is the associated bilinear map for a quadratic map Q. Source of this name: https://en.wikipedia.org/wiki/Quadratic_form#Generalization

Defined in

Mathlib.LinearAlgebra.QuadraticForm.Basic

Cited by

50 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

AddCommGroupAddCommGroup