emultiplicity_eq_coe — Mathlib

English

For any a,b in a monoid and any n ∈ ℕ, the emultiplicity a b equals n if and only if a^n divides b and a^(n+1) does not divide b.

Русский

Пусть a и b — элементы моноида, и n ∈ ℕ. Тогда эмmultiplicity a b равно n тогда и только тогда, когда a^n делит b, и a^(n+1) не делит b.

LaTeX

$$$ \operatorname{emultiplicity}(a,b) = n \iff a^n \mid b \land \neg a^{n+1} \mid b $$$

Lean4

theorem emultiplicity_eq_coe {n : ℕ} : emultiplicity a b = n ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b :=
  by
  constructor
  · intro h
    constructor
    · apply pow_dvd_of_le_emultiplicity
      simp [h]
    · apply not_pow_dvd_of_emultiplicity_lt
      rw [h]
      norm_cast
      simp
  · rw [and_imp]
    apply emultiplicity_eq_of_dvd_of_not_dvd

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