mem_hasEvalIdeal_iff

Mathlib.RingTheory.MvPowerSeries.Evaluation

URI: https://scilib.ai/kg/mathlib#MvPowerSeries.mem_hasEvalIdeal_iff

English

An element a belongs to the hasEvalIdeal if and only if a has evaluation.

Русский

Элемент принадлежит hasEvalIdeal тогда и только тогда, когда он имеет оценку.

LaTeX

$$$a \\in \\text{hasEvalIdeal} \\iff \\text{HasEval } a$$$

Lean4

theorem mem_hasEvalIdeal_iff {a : σ → S} : a ∈ hasEvalIdeal ↔ HasEval a := by simp [hasEvalIdeal]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru