Theorem sq_eq_one

Modification history

2026-01-09 11:59
Mathlib/Algebra/Group/Torsion.lean
refactor: unify the two versions of `pow_eq_one_iff` (#30799) …
Modified sq_eq_oneView on Github →
2025-12-04 09:22
Mathlib/Algebra/Group/Torsion.lean
feat(Tactic): add `lia` as an alias for `cutsat` and use it throughout (#32376) …
Modified sq_eq_oneView on Github →
2025-10-27 08:05
Mathlib/Algebra/Group/Torsion.lean
feat(Algebra/Group/Torsion): characterise when `a ^ n = 1` (#30680)
Modified sq_eq_oneView on Github →
2025-10-17 16:01
Mathlib/Algebra/Group/Torsion.lean
chore(Algebra/Group/EvenFunction): don't import torsion-free modules (#30628) …
Added sq_eq_oneView on Github →