coe_injective

Mathlib.RingTheory.AdjoinRoot

URI: https://scilib.ai/kg/mathlib#AdjoinRoot.coe_injective

English

For a field K and a polynomial f with degree f > 0, the natural map K → AdjoinRoot f is injective.

Русский

Для поля K и полинома f с deg f > 0 естественная карта K → AdjoinRoot f инъективна.

LaTeX

$$Injective(K → AdjoinRoot f) under degree f ≠ 0$$

Lean4

theorem coe_injective (h : degree f ≠ 0) : Function.Injective ((↑) : K → AdjoinRoot f) :=
  have := AdjoinRoot.nontrivial f h
  (of f).injective

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

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

Разделы

Аффилиация

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