divisors_inj

Mathlib.NumberTheory.Divisors

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

English

For all a,b ∈ ℕ, a.divisors = b.divisors iff a = b.

Русский

Для любых a,b ∈ ℕ, a.divisors = b.divisors тогда и только тогда, когда a = b.

LaTeX

$$$ a,b \in \mathbb{N} : a.divisors = b.divisors \iff a = b $$$

Lean4

@[simp]
theorem divisors_inj {a b : ℕ} : a.divisors = b.divisors ↔ a = b :=
  divisors_injective.eq_iff

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

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

Разделы

Аффилиация

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