Theorems · Inductive type · number theory

QuadraticMap

(R : Type u) →
  (M : Type v) →
    (N : Type w) →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] → [Module R M] → [inst_3 : AddCommMonoid N] → [Module R N] → Type (max v w)

A quadratic map on a module. For a more familiar constructor when R is a ring, see QuadraticMap.ofPolar.

Defined in

Mathlib.LinearAlgebra.QuadraticForm.Basic

Cited by

262 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 6 definitions · uses no axioms

Assumes

CommSemiringAddCommMonoidModuleAddCommMonoidModule