Mathlib Map

Theorems · Theorem

Matrix.empty_eq

∀ {α : Type u} (v : Fin 0 → α), v = ![]
Defined in
Mathlib.Data.Fin.VecNotation
Cited by
20 results in Mathlib
Foundations
Depth 10 from the axioms · uses Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Matrix.zero_empty · cited by 34Matrix.zero_emptyMatrix.empty_val' · cited by 11Matrix.empty_val'Matrix.empty_mul · cited by 8Matrix.empty_mulMatrix.smul_empty · cited by 8Matrix.smul_emptyMatrix.neg_empty · cited by 6Matrix.neg_emptyMatrix.finZeroElim_eq_zero · cited by 5Matrix.finZeroElim_eq_zeroTopology.RelCWComplex.closedCell_zero_eq_singleton · cited by 4RelCWComplex.closedCell_z…Matrix.submatrix_empty · cited by 4Matrix.submatrix_emptyTopology.RelCWComplex.openCell_zero_eq_singleton · cited by 3RelCWComplex.openCell_zer…Matrix.empty_add_empty · cited by 3Matrix.empty_add_emptyMatrix.empty_mulVec · cited by 1Matrix.empty_mulVecMatrix.smul_mat_empty · cited by 0Matrix.smul_mat_emptyMatrix.mul_empty · cited by 0Matrix.mul_emptyMatrix.vecMulVec_empty · cited by 0Matrix.vecMulVec_emptyMatrix.replicateCol_empty · cited by 0Matrix.replicateCol_emptyMatrix.vecEmpty · cited by 832Matrix.vecEmptyMatrix.empty_eqCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by20

Results whose statement or proof uses this declaration.