dvd_iff — Mathlib

English

For k,m ∈ ℕ⁺, k ∣ m iff (k : ℕ) ∣ (m : ℕ).

Русский

Для k,m ∈ ℕ⁺, k делит m тогда и только тогда, когда (k) делит (m) как натуральные числа.

LaTeX

$$$$ k \mid m \iff (k : \mathbb{N}) \mid (m : \mathbb{N}) $$$$

Lean4

theorem dvd_iff {k m : ℕ+} : k ∣ m ↔ (k : ℕ) ∣ (m : ℕ) :=
  by
  constructor <;> intro h
  · rcases h with ⟨_, rfl⟩
    apply dvd_mul_right
  · rcases h with ⟨a, h⟩
    obtain ⟨n, rfl⟩ :=
      Nat.exists_eq_succ_of_ne_zero (n := a) <| by
        rintro rfl
        simp only [mul_zero, ne_zero] at h
    use ⟨n.succ, n.succ_pos⟩
    rw [← coe_inj, h, mul_coe, mk_coe]

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