Theorems · Theorem · linear algebra
Matrix.one_mulVec
∀ {m : Type u_2} {α : Type v} [inst : NonAssocSemiring α] [inst_1 : Fintype m] [inst_2 : DecidableEq m] (v : m → α),
Matrix.mulVec 1 v = v- Defined in
- Mathlib.Data.Matrix.Mul
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fintypestatement and proof · cited by 7,736
- Matrixstatement and proof · cited by 4,303
- one_mulproof · cited by 2,841
- NonAssocSemiringstatement and proof · cited by 805
- Matrix.mulVecstatement and proof · cited by 267
- Matrix.diagonal_oneproof · cited by 13
- Matrix.mulVec_diagonalproof · cited by 8
Cited by12
Results whose statement or proof uses this declaration.
- Matrix.Nonsingular.linearIndependent_colproof · cited by 2
- Matrix.mulVec_cramerproof · cited by 2
- Matrix.inv_mulVec_eq_vecproof · cited by 1
- Matrix.IsHermitian.star_eigenvectorUnitary_mulVecproof · cited by 1
- Matrix.mulVec_surjective_iff_exists_right_inverseproof · cited by 1
- Algebra.discr_mul_isIntegral_mem_adjoinproof · cited by 1
- RootPairing.GeckConstruction.ωConjLieSubmodule_eq_top_iffproof · cited by 0
- Matrix.det_eq_zero_of_mulVec_eq_zero_of_mem_nonZeroDivisorsproof · cited by 0
- Matrix.SpecialLinearGroup.transvection_mulVec_single_otherproof · cited by 0
- Matrix.SpecialLinearGroup.transvection_mulVec_single_selfproof · cited by 0
- Matrix.SpecialLinearGroup.transvection_smul_single_fstproof · cited by 0
- Matrix.SpecialLinearGroup.transvection_smul_single_sndproof · cited by 0