exists_eq_pow_mul_and_not_dvd — Mathlib

English

If a finite multiplicity holds for a and b, then there exists c such that b = a^{multiplicity(a,b)} · c and a ∤ c.

Русский

Пусть для a и b выполняется конечная умножимость; тогда существует c such that b = a^{multiplicity(a,b)} · c и a не делит c.

LaTeX

$$$ \exists c \in \alpha\;:\; b = a^{\operatorname{multiplicity}(a,b)} \cdot c \land \lnot a \mid c $$$

Lean4

theorem exists_eq_pow_mul_and_not_dvd (hfin : FiniteMultiplicity a b) :
    ∃ c : α, b = a ^ multiplicity a b * c ∧ ¬a ∣ c :=
  by
  obtain ⟨c, hc⟩ := pow_multiplicity_dvd a b
  refine ⟨c, hc, ?_⟩
  rintro ⟨k, hk⟩
  rw [hk, ← mul_assoc, ← _root_.pow_succ] at hc
  have h₁ : a ^ (multiplicity a b + 1) ∣ b := ⟨k, hc⟩
  exact (hfin.multiplicity_eq_iff.1 (by simp)).2 h₁

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