mem_of_isSquare

Mathlib.Algebra.Order.Ring.Ordering.Defs

URI: https://scilib.ai/kg/mathlib#RingPreordering.mem_of_isSquare

← MathLib Explorer

English

If x is a square in the ring, then x belongs to P.

Русский

Если x является квадратом в кольце, то x принадлежит P.

LaTeX

$$IsSquare(x) \Rightarrow x \in P$$

Lean4

@[aesop unsafe 80% (rule_sets := [SetLike])]
protected theorem mem_of_isSquare (P : RingPreordering R) {x : R} (hx : IsSquare x) : x ∈ P :=
  RingPreordering.mem_of_isSquare' _ hx

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

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

Разделы

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

Аффилиация

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