inclusion_self

Mathlib.FieldTheory.IntermediateField.Basic

URI: https://scilib.ai/kg/mathlib#IntermediateField.inclusion_self

English

The inclusion of a field into itself is the identity map.

Русский

Включение поля в себя есть тождественный гомоморфизм.

LaTeX

$$$ \\text{inclusion}(\\mathrm{le\\_refl}\\, E) = \\mathrm{id}_K E $$$

Lean4

@[simp]
theorem inclusion_self {E : IntermediateField K L} : inclusion (le_refl E) = AlgHom.id K E :=
  Subalgebra.inclusion_self

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

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

Разделы

Аффилиация

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