ramificationIdx_of_not_le

Mathlib.NumberTheory.RamificationInertia.Basic

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

English

If map f p is not ≤ P, then ramificationIdx f p P = 0.

Русский

Если map f p не ≤ P, то ramificationIdx f p P = 0.

LaTeX

$$$\\text{If } ¬(map f p ≤ P) \\text{ then } ramificationIdx f p P = 0$$$

Lean4

@[simp]
theorem ramificationIdx_of_not_le (h : ¬map f p ≤ P) : ramificationIdx f p P = 0 :=
  ramificationIdx_spec (by simp) (by simpa using h)

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

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

Разделы

Аффилиация

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