abs_def — Mathlib

English

For any q ∈ ℚ, |q| = q.num.natAbs / q.den.

Русский

Для любого q ∈ ℚ, |q| = |q.num| / q.den.

LaTeX

$$$|q| = \\dfrac{q.num.natAbs}{q.den}$$$

Lean4

theorem abs_def (q : ℚ) : |q| = q.num.natAbs /. q.den :=
  by
  rcases le_total q 0 with hq | hq
  · rw [abs_of_nonpos hq]
    rw [← num_divInt_den q, ← zero_divInt, Rat.divInt_le_divInt (mod_cast q.pos) Int.zero_lt_one, mul_one,
      zero_mul] at hq
    rw [Int.ofNat_natAbs_of_nonpos hq, ← neg_def]
  · rw [abs_of_nonneg hq]
    rw [← num_divInt_den q, ← zero_divInt, Rat.divInt_le_divInt Int.zero_lt_one (mod_cast q.pos), mul_one,
      zero_mul] at hq
    rw [Int.natAbs_of_nonneg hq, num_divInt_den]

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