instPowSubtypeMemInt

Mathlib.Algebra.Field.Subfield.Defs

URI: https://scilib.ai/kg/mathlib#Subfield.instPowSubtypeMemInt

← MathLib Explorer

English

The zero of a subfield maps to zero in the ambient field; the inclusion preserves zero.

Русский

Ноль подполя отображается в ноль в всём поле; включение сохраняет ноль.

LaTeX

$$$((0 : s) : K) = 0$$$

Lean4

instance : Pow s ℤ :=
  ⟨fun x z => ⟨x ^ z, s.zpow_mem x.2 z⟩⟩
    -- TODO: Those are just special cases of `SubfieldClass.toDivisionRing`/`SubfieldClass.toField`

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

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

Разделы

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

Аффилиация

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