exponent_def

Mathlib.FieldTheory.PurelyInseparable.Exponent

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

← MathLib Explorer

English

If HasExponent K L holds, then IsPurelyInseparable K L holds.

Русский

Если HasExponent K L выполняется, то K ⊆ L является чисто неразделимым (IsPurelyInseparable).

LaTeX

$$HasExponent K L ⇒ IsPurelyInseparable K L$$

Lean4

theorem exponent_def [HasExponent K L] (a : L) : a ^ ringExpChar K ^ exponent K L ∈ (algebraMap K L).range :=
  Nat.find_spec ‹HasExponent K L›.has_exponent a

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

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

Разделы

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

Аффилиация

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