of — Mathlib · SciLib

English

The object in QuadraticModuleCat R associated to a quadratic R-module Q is the object with underlying ModuleCat.of and form Q.

Русский

Объект в QuadraticModuleCat R, соответствующий квадратичному R-модулю Q, имеет основание ModuleCat.of и форму Q.

LaTeX

$${ QuadraticModuleCat.of Q ∈ QuadraticModuleCat R }$$

Lean4

/-- The object in the category of quadratic R-modules associated to a quadratic R-module. -/
abbrev of {X : Type v} [AddCommGroup X] [Module R X] (Q : QuadraticForm R X) : QuadraticModuleCat R :=
  { ModuleCat.of R X with form := Q }

Похожие утверждения