Theorem Subgroup.HasDetPlusMinusOne.isParabolic_iff_of_upperTriangular

Modification history

2025-10-15 06:00
Mathlib/NumberTheory/ModularForms/Cusps.lean
feat(GeneralLinearGroup/FinTwo): the addChar sending x to [1,x;0,1] (#30475)
Added Subgroup.HasDetPlusMinusOne.isParabolic_iff_of_upperTriangularView on Github →