Theorems · Theorem
Matrix.empty_mul
∀ {α : Type u} {n' : Type uₙ} {o' : Type uₒ} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n']
(A : Matrix (Fin 0) n' α) (B : Matrix n' o' α), A * B = Matrix.of ![]- Defined in
- Mathlib.LinearAlgebra.Matrix.Notation
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Equivstatement · cited by 8,337
- Fintypestatement and proof · cited by 7,736
- Matrixstatement and proof · cited by 4,303
- NonUnitalNonAssocSemiringstatement and proof · cited by 1,081
- Matrix.vecEmptystatement · cited by 832
- Matrix.ofstatement · cited by 336
- Matrix.empty_eqproof · cited by 20
Cited by8
Results whose statement or proof uses this declaration.
- ModularGroup.S_mul_S_eqproof · cited by 2
- ModularGroup.T_pow_mul_apply_oneproof · cited by 2
- UpperHalfPlane.J_sqproof · cited by 1
- FixedDetMatrices.reduce_mem_repsproof · cited by 1
- UpperHalfPlane.denom_J_mulproof · cited by 1
- Matrix.of_mem_specialOrthogonalGroup_fin_two_iffproof · cited by 1
- ModularGroup.T_inv_mul_apply_oneproof · cited by 1
- ModularGroup.T_mul_apply_oneproof · cited by 1