ker_evalₗ

Mathlib.FieldTheory.Finite.Polynomial

URI: https://scilib.ai/kg/mathlib#MvPolynomial.ker_evalₗ

← MathLib Explorer

English

As above, ker(evalᵢ) = ⊥.

Русский

Как выше, ker(evalᵢ) = ⊥.

LaTeX

$$$\\\\ker(\\\\mathrm{eval}_{i}) = \\\\{0\\\\}$$$

Lean4

theorem ker_evalₗ [Finite σ] : ker (evalᵢ σ K) = ⊥ :=
  by
  cases nonempty_fintype σ
  refine (ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank ?_).mpr (range_evalᵢ σ K)
  classical rw [Module.finrank_fintype_fun_eq_card, finrank_R]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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