English
A rational q is a square iff both its numerator and denominator (in lowest terms) are squares.
Русский
Рациональное число q является квадратом тогда и только тогда, когда и числитель, и знаменатель в его представлении в виде дроби являются квадратами.
LaTeX
$$IsSquare(q) \iff IsSquare(q.num) \land IsSquare(q.den)$$
Lean4
theorem isSquare_iff {q : ℚ} : IsSquare q ↔ IsSquare q.num ∧ IsSquare q.den :=
by
constructor
· rintro ⟨qr, rfl⟩
rw [Rat.mul_self_num, mul_self_den]
simp only [IsSquare.mul_self, and_self]
· rintro ⟨⟨nr, hnr⟩, ⟨dr, hdr⟩⟩
refine ⟨nr / dr, ?_⟩
rw [div_mul_div_comm, ← Int.cast_mul, ← Nat.cast_mul, ← hnr, ← hdr, num_div_den]
