Theorems · Theorem · number theory
ModularGroup.SL_neg_smul
∀ (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (z : UpperHalfPlane), -g • z = g • z
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 175 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites21
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Realstatement and proof · cited by 25,697
- Units.valproof · cited by 1,966
- neg_negproof · cited by 960
- UpperHalfPlanestatement and proof · cited by 626
- Matrix.GeneralLinearGroupproof · cited by 556
- Matrix.extproof · cited by 540
- Matrix.SpecialLinearGroupstatement and proof · cited by 348
- Int.castRingHomproof · cited by 254
- Matrix.mapproof · cited by 247
- Matrix.SpecialLinearGroup.mapGLproof · cited by 98
- Units.extproof · cited by 86
Cited by5
Results whose statement or proof uses this declaration.
- ModularGroup.cases_of_mem_fd_smul_mem_fdproof · cited by 2
- ModularGroup.exists_eq_T_zpow_of_c_eq_zeroproof · cited by 0
- ModularGroup.stabilizer_Iproof · cited by 0
- ModularGroup.stabilizer_ρproof · cited by 0
- ModularGroup.eq_smul_self_of_mem_fdo_mem_fdoproof · cited by 0