dimension — Mathlib

English

The dimension of a presentation is the number of generators minus the number of relations.

Русский

У размерности презентaции — число порождающих минус число отношений.

LaTeX

$$$\\dim(P) = |\\iota| - |\\sigma|$$$

Lean4

/-- Dimension of a presentation defined as the cardinality of the generators
minus the cardinality of the relations.

Note: this definition is completely non-sensical for non-finite presentations and
even then for this to make sense, you should assume that the presentation
is a complete intersection.
-/
@[nolint unusedArguments]
noncomputable def dimension (P : Presentation R S ι σ) : ℕ :=
  Nat.card ι - Nat.card σ

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