Mathlib Map

Theorems · Theorem · group theory

isSquare_inv

∀ {α : Type u_2} [inst : DivisionMonoid α] {a : α}, IsSquare a⁻¹ ↔ IsSquare a
Defined in
Mathlib.Algebra.Group.Even
Cited by
2 results in Mathlib
Foundations
Depth 20 from the axioms · uses propext, Quot.sound
Assumes
DivisionMonoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

IsSquare.inv · cited by 0IsSquare.invisSquare_mabs · cited by 0isSquare_mabsMulOpposite.op · cited by 520MulOpposite.opinv_inv · cited by 494inv_invMulEquiv.symm · cited by 482MulEquiv.symmDivisionMonoid · cited by 201DivisionMonoidIsSquare · cited by 132IsSquareMulEquiv.inv' · cited by 4MulEquiv.inv'IsSquare.map · cited by 3IsSquare.mapisSquare_op_iff · cited by 2isSquare_op_iffMulEquiv.inv'_symm_apply · cited by 1MulEquiv.inv'_symm_applyisSquare_invCITED BYCITES

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.