Theorems · Theorem · group theory
Matrix.SpecialLinearGroup.coeToGL_det
∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R]
(g : Matrix.SpecialLinearGroup n R), Matrix.GeneralLinearGroup.det (Matrix.SpecialLinearGroup.toGL g) = 1- Cited by
- 10 results in Mathlib
- Foundations
- Depth 107 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableEqFintypeCommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- Fintypestatement and proof · cited by 7,736
- Matrixstatement · cited by 4,303
- MonoidHomstatement · cited by 3,629
- Unitsstatement · cited by 2,804
- Matrix.GeneralLinearGroupstatement · cited by 556
- Subtype.propproof · cited by 505
- Matrix.SpecialLinearGroupstatement and proof · cited by 348
- Units.extproof · cited by 86
- Matrix.SpecialLinearGroup.toGLstatement · cited by 64
- Matrix.GeneralLinearGroup.detstatement · cited by 58
Cited by10
Results whose statement or proof uses this declaration.
- ModularForm.SL_slash_applyproof · cited by 7
- ModularGroup.im_smul_eq_div_normSqproof · cited by 6
- ModularForm.SL_slash_defproof · cited by 2
- ModularForm.is_invariant_constproof · cited by 1
- Matrix.SpecialLinearGroup.det_mapGLproof · cited by 1
- Derivative.normalizedDerivOfComplex_SL_slashproof · cited by 1
- Matrix.SpecialLinearGroup.toGL_mem_center_iffproof · cited by 0
- ModularForm.mul_slash_SL2proof · cited by 0
- UpperHalfPlane.petersson_slash_SLproof · cited by 0
- Matrix.ProjectiveSpecialLinearGroup.toPGL_surj_iffproof · cited by 0