core — Mathlib

English

The core of a presentation is the subalgebra generated by the coefficients of the relations.

Русский

Ядро презентации — это подалгебра, порождаемая коэффициентами отношений.

LaTeX

$$$\\mathrm{core}:= \\mathrm{Algebra.adjoin}\\_{}\\; _{\\mathbb{Z}}\\; P.coeffs$$$

Lean4

/-- The core of a presentation is the subalgebra generated by the coefficients of the relations. -/
def core : Subalgebra ℤ R :=
  Algebra.adjoin _ P.coeffs

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