multiplicity_le_of_emultiplicity_le

Mathlib.RingTheory.Multiplicity

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

← MathLib Explorer

English

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

Русский

Если emultiplicity a b ≤ n, то multiplicity a b ≤ n.

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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