Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_torsion.exponent_exists

Modification history

2022-02-25 22:23

src/group_theory/torsion.lean

feat(group_theory/torsion): define torsion groups (#11850) …

Added is_torsion.exponent_exists View on Github →