sup_divisors_id — Mathlib

English

The supremum (largest element) of divisors of n is n: divisors of n, when ordered by size, have maximum n.

Русский

Наибольший делитель числа n равен n.

LaTeX

$$$\\max\\{d: d\\mid n\\} = n$$$

Lean4

@[simp]
theorem sup_divisors_id (n : ℕ) : n.divisors.sup id = n :=
  by
  refine le_antisymm (Finset.sup_le fun _ ↦ divisor_le) ?_
  rcases Decidable.eq_or_ne n 0 with rfl | hn
  · apply zero_le
  · exact Finset.le_sup (f := id) <| mem_divisors_self n hn

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