le_emultiplicity_of_le_multiplicity

Mathlib.RingTheory.Multiplicity

URI: https://scilib.ai/kg/mathlib#le_emultiplicity_of_le_multiplicity

← MathLib Explorer

English

If n ≤ multiplicity a b, then n ≤ emultiplicity a b.

Русский

Если n ≤ кратность(a,b), то n ≤ эммultiplicity(a,b).

LaTeX

$$$ n \le multiplicity(a,b) \Rightarrow n \le emultiplicity(a,b) $$$

Lean4

theorem le_emultiplicity_of_le_multiplicity {n : ℕ} (h : n ≤ multiplicity a b) : n ≤ emultiplicity a b := by
  exact_mod_cast (WithTop.coe_mono h).trans multiplicity_le_emultiplicity

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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