emultiplicity_pos_iff

Mathlib.RingTheory.Multiplicity

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

← MathLib Explorer

English

0 < emultiplicity a b is equivalent to 0 < multiplicity a b.

Русский

0 < эмплитичность a b эквивалентно 0 < кратности a b.

LaTeX

$$$$0 < emultiplicity\ a\ b \leftrightarrow 0 < multiplicity\ a\ b.$$$$

Lean4

theorem emultiplicity_pos_iff : 0 < emultiplicity a b ↔ 0 < multiplicity a b := by
  simp [pos_iff_ne_zero, pos_iff_ne_zero, emultiplicity_eq_zero_iff_multiplicity_eq_zero]

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

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

Разделы

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

Аффилиация

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