isSquare_intCast_iff

Mathlib.Data.Rat.Lemmas

URI: https://scilib.ai/kg/mathlib#Rat.isSquare_intCast_iff

← MathLib Explorer

English

For integers z, IsSquare(z as rational) iff IsSquare z.

Русский

Для целых z: IsSquare(z в рационе) эквивалентно IsSquare z.

LaTeX

$$IsSquare(z) (as rational) \iff IsSquare(z)$$

Lean4

@[norm_cast, simp]
theorem isSquare_intCast_iff {z : ℤ} : IsSquare (z : ℚ) ↔ IsSquare z := by
  simp_rw [isSquare_iff, num_intCast, den_intCast, IsSquare.one, and_true]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru