elemExponent_eq_zero_of_mem_range

Mathlib.FieldTheory.PurelyInseparable.Exponent

URI: https://scilib.ai/kg/mathlib#IsPurelyInseparable.elemExponent_eq_zero_of_mem_range

← MathLib Explorer

English

If a ∈ range(algebraMap K L), then elemExponent K a = 0.

Русский

Если a ∈ range(algebraMap K L), то elemExponent K a = 0.

LaTeX

$$elemExponent K a = 0$$

Lean4

theorem elemExponent_eq_zero_of_mem_range {a : L} (h : a ∈ (algebraMap K L).range) : elemExponent K a = 0 :=
  by
  apply (Nat.find_eq_zero _).mpr
  rw [pow_zero, pow_one]
  obtain ⟨y, hy⟩ := h
  exact ⟨y, hy ▸ minpoly.eq_X_sub_C L y⟩

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

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

Разделы

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

Аффилиация

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