modOf — Mathlib

English

Define the remainder modOf x by g as the part of x that cannot be further reduced by subtracting multiples of the basis element corresponding to g.

Русский

Определим остаток modOf x по g как часть x, которая не может быть далее сведена путем вычитания кратных базисному элементу g.

LaTeX

$$$\\operatorname{modOf}:\\ k[G] \\to \\ k[G] \\quad (x,g) \\mapsto x.filter\\,\\{ g_1 \\mid \\neg \\exists d, g_1 = g + d \\}$$$

Lean4

/-- The remainder upon division by `of' k G g`. -/
noncomputable def modOf (x : k[G]) (g : G) : k[G] :=
  letI := Classical.decPred fun g₁ => ∃ g₂, g₁ = g + g₂
  x.filter fun g₁ => ¬∃ g₂, g₁ = g + g₂

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