Theorem sq_eq_one

Modification history

2025-10-27 08:05

Mathlib/Algebra/Group/Torsion.lean

feat(Algebra/Group/Torsion): characterise when `a ^ n = 1` (#30680)

Modified sq_eq_one View 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_one View on Github →