Theorems · Definition · group theory
Matrix.GeneralLinearGroup.scalar
(n : Type u) → [inst : DecidableEq n] → [inst_1 : Fintype n] → {R : Type v} → [inst_2 : Semiring R] → Rˣ →* GL n RScalar matrix as an element of GL n R.
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableEqFintypeSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement and proof · cited by 13,802
- 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
- RingHom.toMonoidHomproof · cited by 132
- Units.mapproof · cited by 95
- Matrix.scalarproof · cited by 62
Cited by20
Results whose statement or proof uses this declaration.
- Matrix.GeneralLinearGroup.center_eq_range_scalarstatement and proof · cited by 6
- Matrix.GeneralLinearGroup.det_scalarstatement and proof · cited by 3
- Matrix.ProjGenLinGroup.liftstatement and proof · cited by 2
- UpperHalfPlane.glScalar_smulstatement and proof · cited by 2
- UpperHalfPlane.num_scalarstatement · cited by 1
- Matrix.ProjGenLinGroup.mk_smulstatement and proof · cited by 1
- Matrix.ProjGenLinGroup.mulActionOfGLstatement and proof · cited by 1
- UpperHalfPlane.denom_scalarstatement · cited by 1
- Matrix.GeneralLinearGroup.map_scalarstatement and proof · cited by 1
- Matrix.GeneralLinearGroup.coe_scalarstatement · cited by 1
- Matrix.ProjGenLinGroup.mk_eq_mk_iffstatement and proof · cited by 0
- Matrix.ProjGenLinGroup.mk_scalarstatement and proof · cited by 0