range_evalᵢ

Mathlib.FieldTheory.Finite.Polynomial

URI: https://scilib.ai/kg/mathlib#MvPolynomial.range_evalᵢ

English

As above, the evaluation map eval_i has full range when σ is finite.

Русский

Как выше, отображение eval_i имеет полный образ при конечном σ.

LaTeX

$$$\\\\mathrm{range}(\\\\mathrm{eval}_{i}) = \\\\top$$$

Lean4

theorem range_evalᵢ [Finite σ] : range (evalᵢ σ K) = ⊤ :=
  by
  rw [evalᵢ, LinearMap.range_comp, range_subtype]
  exact map_restrict_dom_evalₗ K σ

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

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

Разделы

Аффилиация

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