isSquare_unop_iff — Mathlib

English

Let a be an element of αᵐᵒᵖ. Then a is a square in αᵐᵒᵖ if and only if unop a is a square in α.

Русский

Пусть a принадлежит αᵐᵒᵖ. Тогда a является квадратом в αᵐᵒᵖ тогда и только тогда, когда unop a является квадратом в α.

LaTeX

$$$\forall a : \alpha^{\mathrm{op}}, \operatorname{IsSquare}(\mathrm{unop}(a)) \iff \operatorname{IsSquare}(a)$$$

Lean4

@[to_additive]
theorem isSquare_unop_iff {a : αᵐᵒᵖ} : IsSquare (unop a) ↔ IsSquare a :=
  isSquare_op_iff.symm

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