isSquare_iff_exists_sq

Mathlib.Algebra.Group.Even

URI: https://scilib.ai/kg/mathlib#isSquare_iff_exists_sq

English

In a monoid, IsSquare a is equivalent to there exists r with a = r^2.

Русский

В моноиде IsSquare a эквивалентно существованию r: a = r^2.

LaTeX

$$$\operatorname{IsSquare}(a) \iff \exists r, a = r^2$$$

Lean4

@[to_additive even_iff_exists_two_nsmul]
theorem isSquare_iff_exists_sq (a : α) : IsSquare a ↔ ∃ r, a = r ^ 2 := by simp [IsSquare, pow_two]

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

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

Разделы

Аффилиация

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