emultiplicity_eq_emultiplicity_iff

English

emultiplicity a b = emultiplicity c d if and only if for all n, a^n ∣ b ↔ c^n ∣ d.

Русский

emultiplicity a b = emultiplicity c d эквивалентно тому, что для всех n, a^n ∣ b ↔ c^n ∣ d.

LaTeX

$$$ \operatorname{emultiplicity}(a,b) = \operatorname{emultiplicity}(c,d) \iff \forall n \in \mathbb{N},\ a^n \mid b \iff c^n \mid d$$$

Lean4

theorem emultiplicity_eq_emultiplicity_iff {c d : β} :
    emultiplicity a b = emultiplicity c d ↔ ∀ n : ℕ, a ^ n ∣ b ↔ c ^ n ∣ d :=
  ⟨fun h n => ⟨emultiplicity_le_emultiplicity_iff.1 h.le n, emultiplicity_le_emultiplicity_iff.1 h.ge n⟩, fun h =>
    le_antisymm (emultiplicity_le_emultiplicity_iff.2 fun n => (h n).mp)
      (emultiplicity_le_emultiplicity_iff.2 fun n => (h n).mpr)⟩

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