Theorems · Definition · group theory
Matrix.SpecialLinearGroup.diag2
{F : Type u_1} → [inst : Field F] → (a : F) → a ≠ 0 → Matrix.SpecialLinearGroup (Fin 2) FAn element in SL₂(F) induced by a diagonal matrix with a, a⁻¹ on
positition 0 and 1 respectively.
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Field
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fieldstatement and proof · cited by 7,404
- Matrix.SpecialLinearGroupstatement · cited by 348
- Matrix.SpecialLinearGroup.diag2nproof · cited by 7
Cited by13
Results whose statement or proof uses this declaration.
- Matrix.SpecialLinearGroup.diag2_coestatement · cited by 5
- Matrix.SL2.transvection_inductionproof · cited by 2
- Matrix.SpecialLinearGroup.diag2_invstatement · cited by 2
- Matrix.SpecialLinearGroup.diag2.congr_simpstatement and proof · cited by 1
- Matrix.transvection_mem_commutator₀proof · cited by 1
- Matrix.transvection_mem_commutator₁proof · cited by 1
- Matrix.SpecialLinearGroup.diag2_coe'statement · cited by 1
- Matrix.diag2_decomposestatement and proof · cited by 1
- Matrix.SpecialLinearGroup.diag2_mul_invstatement · cited by 1
- Matrix.commutator_diag2_transvectionstatement and proof · cited by 1
- Matrix.SpecialLinearGroup.diag2_smul_single_i₂statement · cited by 0
- Matrix.SpecialLinearGroup.diag2_defstatement · cited by 0