Theorems · Theorem · number theory
Subgroup.HasDetPlusMinusOne.abs_det
∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_2} [inst_2 : CommRing R]
{Γ : Subgroup (GL n R)} [inst_3 : LinearOrder R] [IsOrderedRing R] [Γ.HasDetPlusMinusOne] {g : GL n R},
g ∈ Γ → |↑(Matrix.GeneralLinearGroup.det g)| = 1- Cited by
- 2 results in Mathlib
- Foundations
- Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- LinearOrderstatement and proof · cited by 8,572
- Fintypestatement and proof · cited by 7,736
- Matrixstatement · cited by 4,303
- MonoidHomstatement · cited by 3,629
- Subgroupstatement and proof · cited by 3,593
- Unitsstatement · cited by 2,804
- Units.valstatement and proof · cited by 1,966
- absstatement and proof · cited by 1,814
- IsOrderedRingstatement and proof · cited by 777
- Matrix.GeneralLinearGroupstatement and proof · cited by 556
Cited by2
Results whose statement or proof uses this declaration.
- SlashInvariantFormClass.norm_petersson_smulproof · cited by 2
- Subgroup.hasDetPlusMinusOne_iff_abs_detproof · cited by 0