Theorems · Theorem · general topology
Matrix.fin_two_smul_prod
Deprecated since 2026-04-19Mathlib marks this declaration as deprecated.
∀ {R : Type u_1} [inst : Semiring R] (g : Matrix (Fin 2) (Fin 2) R) (v : R × R),
g • v = (g 0 0 * v.1 + g 0 1 * v.2, g 1 0 * v.1 + g 1 1 * v.2)- Cited by
- 1 results in Mathlib
- Foundations
- Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Semiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites22
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Semiringstatement and proof · cited by 13,802
- Matrixstatement and proof · cited by 4,303
- Equiv.symmproof · cited by 3,681
- LinearEquiv.symmproof · cited by 1,461
- LinearEquiv.toLinearMapproof · cited by 1,171
- Matrix.vecConsproof · cited by 852
- Matrix.vecEmptyproof · cited by 832
- MulOpposite.opproof · cited by 520
- Matrix.transposeproof · cited by 389
- Matrix.cons_val_fin_oneproof · cited by 225
- AddHom.toFunproof · cited by 168
Cited by1
Results whose statement or proof uses this declaration.
- Matrix.GeneralLinearGroup.fin_two_smul_prodproof · cited by 0