Theorems · Definition · category theory

QuadraticModuleCat.of

{R : Type u} →
  [inst : CommRing R] →
    {X : Type v} → [inst_1 : AddCommGroup X] → [inst_2 : Module R X] → QuadraticForm R X → QuadraticModuleCat R

The object in the category of quadratic R-modules associated to a quadratic R-module.

Defined in

Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat

Cited by

5 results in Mathlib

Foundations

Depth 16 from the axioms · uses no axioms

Assumes

CommRingAddCommGroupModule