mul_self_num — Mathlib

English

For any rational q, (q * q).num equals q.num * q.num.

Русский

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

LaTeX

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

Lean4

theorem mul_self_num (q : ℚ) : (q * q).num = q.num * q.num :=
  by
  rw [mul_num, Int.natAbs_mul, Nat.Coprime.gcd_eq_one, Int.ofNat_one, Int.ediv_one]
  exact (q.reduced.mul_right q.reduced).mul_left (q.reduced.mul_right q.reduced)

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