Theorem ModularGroup.eq_one_or_neg_one_of_mem_fdo_mem_fdo

Modification history

2026-04-06 13:17
Mathlib/NumberTheory/Modular.lean
feat(NumberTheory/Modular): strengthen 2nd Fundamental-Domain Lemma (#36736) …
Added ModularGroup.eq_one_or_neg_one_of_mem_fdo_mem_fdoView on Github →