Absolute_Value_of_Integer_is_not_less_than_Divisors
Proveddivisorsnumber-theoryproofwiki
A nonzero integer is greater than or equal to its divisors in magnitude.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Absolute_Value_of_Integer_is_not_less_than_Divisors (a c : ℤ) (hc : c ≠ 0) (h : a ∣ c) : Int.natAbs a ≤ Int.natAbs c := by sorry
Source