hasEvalIdeal — Mathlib

English

The set of evaluable elements forms an ideal of the codomain.

Русский

Множество элементов, имеющих оценку, образует идеал окружности, т.е. идеал в S.

LaTeX

$$$\{ a \in S \mid HasEval a \}$ является идеалом в S$$

Lean4

/-- The domain of evaluation of `MvPowerSeries`, as an ideal -/
@[simps]
def hasEvalIdeal : Ideal S where
  carrier := {a | HasEval a}
  add_mem' := HasEval.add
  zero_mem' := HasEval.zero
  smul_mem' := HasEval.mul_left

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