nat_coe_dvd_iff — Mathlib

English

For natural numbers n,m, (n : Cardinal) divides m if and only if n divides m.

Русский

Для натуральных чисел n,m выполняется: (n : Cardinal) делит m тогда и только тогда, когда n делит m.

LaTeX

$$$(n : \mathrm{Cardinal}) \mid m \iff n \mid m$$$

Lean4

@[simp, norm_cast]
theorem nat_coe_dvd_iff : (n : Cardinal) ∣ m ↔ n ∣ m :=
  by
  refine ⟨?_, fun ⟨h, ht⟩ => ⟨h, mod_cast ht⟩⟩
  rintro ⟨k, hk⟩
  have : ↑m < ℵ₀ := nat_lt_aleph0 m
  rw [hk, mul_lt_aleph0_iff] at this
  rcases this with (h | h | ⟨-, hk'⟩)
  iterate 2 simp only [h, mul_zero, zero_mul, Nat.cast_eq_zero] at hk; simp [hk]
  lift k to ℕ using hk'
  exact ⟨k, mod_cast hk⟩

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