isSquare_inv

Mathlib.Algebra.Group.Even

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

← MathLib Explorer

English

In a division monoid, IsSquare a is equivalent to IsSquare a⁻¹.

Русский

В дивизионном моноиде IsSquare a эквивалентно IsSquare a⁻¹.

LaTeX

$$$\operatorname{IsSquare}(a^{-1}) \iff \operatorname{IsSquare}(a)$$$

Lean4

@[to_additive (attr := simp)]
theorem isSquare_inv : IsSquare a⁻¹ ↔ IsSquare a := by
  constructor <;> intro h <;> simpa using (isSquare_op_iff.mpr h).map (MulEquiv.inv' α).symm

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

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

Разделы

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

Аффилиация

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