lift_injective

Mathlib.FieldTheory.IntermediateField.Basic

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

English

The lift operation is injective in its first argument: F.lift is injective in F.

Русский

Операция поднятия инъективна по первому аргументу: F.lift инъективна по F.

LaTeX

$$Function.Injective F.lift$$

Lean4

theorem lift_injective (F : IntermediateField K L) : Function.Injective F.lift :=
  map_injective F.val

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

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

Разделы

Аффилиация

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