not_isSquare

Mathlib.Algebra.Group.Irreducible.Lemmas

URI: https://scilib.ai/kg/mathlib#Irreducible.not_isSquare

← MathLib Explorer

English

If x is irreducible, then x is not a square.

Русский

Если x неразложим, то x не является квадратом.

LaTeX

$$$\\\\forall {M} [Monoid M] {x : M}, \\\\operatorname{Irreducible} x \\\\rightarrow \\\\neg IsSquare x$$$

Lean4

@[to_additive]
theorem not_isSquare (ha : Irreducible x) : ¬IsSquare x :=
  by
  rw [isSquare_iff_exists_sq]
  rintro ⟨y, rfl⟩
  exact not_irreducible_pow (by decide) ha

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

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

Разделы

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

Аффилиация

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