Theorems · Definition · linear algebra
LinearMap.GeneralLinearGroup
(R : Type u_1) → (M : Type u_2) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Type u_2
The group of invertible linear maps from M to itself
- Cited by
- 27 results in Mathlib
- Foundations
- Depth 27 from the axioms · uses propext, Quot.sound
- Assumes
- SemiringAddCommMonoidModule
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- RingHom.idproof · cited by 18,349
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- LinearMapproof · cited by 10,215
- Unitsproof · cited by 2,804
Cited by36
Results whose statement or proof uses this declaration.
- LinearMap.GeneralLinearGroup.toLinearEquivstatement and proof · cited by 9
- LinearMap.GeneralLinearGroup.generalLinearEquivstatement and proof · cited by 7
- LinearMap.GeneralLinearGroup.ofLinearEquivstatement · cited by 6
- LinearMap.GeneralLinearGroup.congrLinearEquivstatement · cited by 5
- SpecialLinearGroup.toGeneralLinearGroupstatement · cited by 4
- Matrix.GeneralLinearGroup.toLinstatement · cited by 4
- Matrix.UnitaryGroup.toGLstatement · cited by 3
- ModularGroup.lcRow0Extend_applystatement · cited by 1
- SpecialLinearGroup.toGeneralLinearGroup_toLinearEquiv_applystatement · cited by 1
- LinearMap.GeneralLinearGroup.generalLinearEquiv_to_linearMapstatement and proof · cited by 1
- Matrix.GeneralLinearGroup.toLin'statement · cited by 1
- Projectivization.generalLinearGroup_smul_defstatement and proof · cited by 0