isSquare_ofNat_iff

Mathlib.Algebra.Ring.Int.Parity

URI: https://scilib.ai/kg/mathlib#Int.isSquare_ofNat_iff

English

For any n ∈ ℕ, IsSquare((ofNat n : ℤ)) ↔ IsSquare((ofNat n : ℕ)).

Русский

Для любого n ∈ ℕ, IsSquare((ofNat n) : ℤ) ⇔ IsSquare(ofNat n).

LaTeX

$$IsSquare((n : \mathbb{Z})) \leftrightarrow IsSquare(n)$$

Lean4

@[simp]
theorem isSquare_ofNat_iff {n : ℕ} : IsSquare (ofNat(n) : ℤ) ↔ IsSquare (ofNat(n) : ℕ) :=
  isSquare_natCast_iff

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

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

Разделы

Аффилиация

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