dvd_iff' — Mathlib

English

For k,m ∈ ℕ⁺, k ∣ m iff mod m k = k.

Русский

Для k,m ∈ ℕ⁺, k делит m тогда и только тогда, когда m mod k = k.

LaTeX

$$$$ k \mid m \iff \operatorname{mod}(m,k) = k $$$$

Lean4

theorem dvd_iff' {k m : ℕ+} : k ∣ m ↔ mod m k = k := by
  rw [dvd_iff]
  rw [Nat.dvd_iff_mod_eq_zero]; constructor
  · intro h
    apply PNat.eq
    rw [mod_coe, if_pos h]
  · intro h
    by_cases h' : (m : ℕ) % (k : ℕ) = 0
    · exact h'
    · replace h : (mod m k : ℕ) = (k : ℕ) := congr_arg _ h
      rw [mod_coe, if_neg h'] at h
      exact ((Nat.mod_lt (m : ℕ) k.pos).ne h).elim

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