emultiplicity_self — Mathlib

English

If a has FiniteMultiplicity a a, then emultiplicity a a = 1; i.e., the a-adic emultiplicity of a relative to itself is 1.

Русский

Если для элемента a выполнима FiniteMultiplicity a a, то эмп-множительность a относительно самого себя равна 1.

LaTeX

$$$ emultiplicity a a = 1 $$$

Lean4

@[simp]
theorem emultiplicity_self {a : α} (hfin : FiniteMultiplicity a a) : emultiplicity a a = 1 := by
  simp [hfin.emultiplicity_eq_multiplicity]

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