dvd_left_iff_eq

Mathlib.Data.Nat.Init

URI: https://scilib.ai/kg/mathlib#Nat.dvd_left_iff_eq

Lean4

/-- Two natural numbers are equal if and only if they have the same divisors. -/
theorem dvd_left_iff_eq : (∀ a : ℕ, a ∣ m ↔ a ∣ n) ↔ m = n :=
  ⟨fun h => Nat.dvd_antisymm ((h _).mp (Nat.dvd_refl _)) ((h _).mpr (Nat.dvd_refl _)), fun h n => by rw [h]⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru