sq

Mathlib.Algebra.Group.Even

URI: https://scilib.ai/kg/mathlib#IsSquare.sq

English

For any r in α, r^2 is a square.

Русский

Для любого r ∈ α, r^2 является квадратом.

LaTeX

$$$\operatorname{IsSquare}(r^2)$$$

Lean4

@[to_additive (attr := aesop safe) Even.two_nsmul]
theorem sq (r : α) : IsSquare (r ^ 2) :=
  ⟨r, pow_two _⟩

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

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

Разделы

Аффилиация

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