inclusion_injective

Mathlib.FieldTheory.IntermediateField.Basic

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

English

If E ≤ F are intermediate fields, the inclusion map from E to F is injective.

Русский

Если E ≤ F — промежуточные поля, то включение E в F инъективно.

LaTeX

$$Inclusion(hEF) is injective$$

Lean4

theorem inclusion_injective {E F : IntermediateField K L} (hEF : E ≤ F) : Function.Injective (inclusion hEF) :=
  Subalgebra.inclusion_injective hEF

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

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

Разделы

Аффилиация

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