multiplicity_eq_iff — Mathlib

English

For a finite multiplicity situation, multiplicity a b equals n iff a^n divides b and a^{n+1} does not divide b.

Русский

При конечной мультипликативности равенство мультипликативности a b = n эквивалентно тому, что a^n делит b, а a^{n+1} не делит b.

LaTeX

$$multiplicity_eq_iff hf {n} : multiplicity a b = n ↔ a^n ∣ b ∧ ¬a^{n+1} ∣ b$$

Lean4

theorem multiplicity_eq_iff (hf : FiniteMultiplicity a b) {n : ℕ} :
    multiplicity a b = n ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b := by
  simp [← emultiplicity_eq_coe, hf.emultiplicity_eq_multiplicity]

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