Theorems · Definition · group theory
Matrix.GeneralLinearGroup.det
{n : Type u} → [inst : DecidableEq n] → [inst_1 : Fintype n] → {R : Type v} → [inst_2 : CommRing R] → GL n R →* RˣThe determinant of a unit matrix is itself a unit.
- Cited by
- 58 results in Mathlib
- Foundations
- Depth 94 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.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- 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
- Units.valproof · cited by 1,966
- Matrix.detproof · cited by 665
- Matrix.GeneralLinearGroupstatement and proof · cited by 556
Cited by66
Results whose statement or proof uses this declaration.
- UpperHalfPlane.σproof · cited by 31
- Matrix.GeneralLinearGroup.val_det_applystatement and proof · cited by 31
- Matrix.GLPosproof · cited by 16
- Matrix.GeneralLinearGroup.det_ne_zeroproof · cited by 13
- Matrix.SpecialLinearGroup.coeToGL_detstatement · cited by 10
- UpperHalfPlane.coe_smul_of_det_posstatement and proof · cited by 4
- UpperHalfPlane.denom_ne_zero_of_improof · cited by 4
- UpperHalfPlane.σ_ofRealproof · cited by 4
- UpperHalfPlane.moebius_imstatement · cited by 3
- UpperHalfPlane.norm_σproof · cited by 3
- UpperHalfPlane.petersson_slashstatement and proof · cited by 3
- UpperHalfPlane.smulFDerivproof · cited by 3