le_comap_pow_ramificationIdx

Mathlib.NumberTheory.RamificationInertia.Basic

URI: https://scilib.ai/kg/mathlib#Ideal.le_comap_pow_ramificationIdx

English

If not (map f p ≤ P) then ramificationIdx equals 0.

Русский

Если не выполняется map f p ≤ P, тогда ramificationIdx равен 0.

LaTeX

$$$¬(map f p ≤ P) \\Rightarrow ramificationIdx f p P = 0$$$

Lean4

theorem le_comap_pow_ramificationIdx : p ≤ comap f (P ^ ramificationIdx f p P) :=
  map_le_iff_le_comap.mp le_pow_ramificationIdx

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

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

Разделы

Аффилиация

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