emultiplicity_eq_top

Mathlib.RingTheory.Multiplicity

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

English

emultiplicity(a,b) equals top precisely when FiniteMultiplicity(a,b) is false.

Русский

emultiplicity(a,b) равна верхнему элементу тогда и только тогда, когда FiniteMultiplicity(a,b) ложно.

LaTeX

$$$ emultiplicity(a,b) = \top \iff \lnot FiniteMultiplicity(a,b) $$$

Lean4

@[simp]
theorem emultiplicity_eq_top : emultiplicity a b = ⊤ ↔ ¬FiniteMultiplicity a b := by simp [emultiplicity]

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

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

Разделы

Аффилиация

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