one_right

Mathlib.RingTheory.Multiplicity

URI: https://scilib.ai/kg/mathlib#FiniteMultiplicity.one_right

English

If ha is a FiniteMultiplicity a 1, then multiplicity a 1 = 0.

Русский

Пусть ha — FiniteMultiplicity a 1; тогда multiplicity a 1 = 0.

LaTeX

$$$ \operatorname{multiplicity}(a,1) = 0 $$$

Lean4

@[simp]
theorem one_right (ha : FiniteMultiplicity a 1) : multiplicity a 1 = 0 := by
  simp [ha.multiplicity_eq_iff, ha.not_dvd_of_one_right]

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

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

Разделы

Аффилиация

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