R — Mathlib · SciLib

English

Define R(σ, K) to be the subspace restrictDegree(σ, K, |K| − 1).

Русский

Определим R(σ, K) как подпространство restrictDegree(σ, K, |K| − 1).

LaTeX

$$$R(\\\\sigma, K) = \\mathrm{restrictDegree}(\\\\sigma, K, |K| - 1).$$$

Lean4

/-- The submodule of multivariate polynomials whose degree of each variable is strictly less
than the cardinality of K. -/
def R [CommRing K] : Type u :=
  restrictDegree σ K
    (Fintype.card K - 1)
      -- The `AddCommGroup, Module K, Inhabited` instances should be constructed by a deriving handler.

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