mul_self_den — Mathlib

English

For any rational q, (q * q).den equals q.den squared.

Русский

Для любого рационального числа q, знаменатель q^2 равен квадрату знаменателя q.

LaTeX

$$$(q \cdot q).den = q.den \cdot q.den$$$

Lean4

theorem mul_self_den (q : ℚ) : (q * q).den = q.den * q.den :=
  by
  rw [Rat.mul_den, Int.natAbs_mul, Nat.Coprime.gcd_eq_one, Nat.div_one]
  exact (q.reduced.mul_right q.reduced).mul_left (q.reduced.mul_right q.reduced)

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