ne_zero

Mathlib.RingTheory.Multiplicity

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

English

In a monoid with zero, if FiniteMultiplicity a b holds, then b ≠ 0.

Русский

В моноиде с нулём, если FiniteMultiplicity a b выполняется, то b ≠ 0.

LaTeX

$$$\\operatorname{FiniteMultiplicity}(a,b) \\Rightarrow b \\neq 0$$$

Lean4

theorem ne_zero {a b : α} (h : FiniteMultiplicity a b) : b ≠ 0 :=
  let ⟨n, hn⟩ := h
  fun hb => by simp [hb] at hn

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

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

Разделы

Аффилиация

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