Mathlib Map

Theorems · Theorem

Matrix.cons_val_fin_one

∀ {α : Type u} (x : α) (u : Fin 0 → α) (i : Fin 1), Matrix.vecCons x u i = x
Defined in
Mathlib.Data.Fin.VecNotation
Cited by
225 results in Mathlib
Foundations
Depth 32 from the axioms, rests on 252 definitions · uses propext
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

WeierstrassCurve.Projective.smul_fin3 · cited by 14Projective.smul_fin3LinearIndependent.pair_iff · cited by 10LinearIndependent.pair_iffUpperHalfPlane.modular_S_smul · cited by 9UpperHalfPlane.modular_S_…Height.mulHeight₁_eq_mulHeight · cited by 6Height.mulHeight₁_eq_mulH…FirstOrder.Language.BoundedFormula.realize_rel₂ · cited by 6BoundedFormula.realize_re…Orientation.eq_or_eq_neg_of_isEmpty · cited by 6Orientation.eq_or_eq_neg_…Complex.coe_basisOneI · cited by 5Complex.coe_basisOneISubgroup.strictWidthInfty_pos_iff · cited by 5Subgroup.strictWidthInfty…Matrix.cons_fin_one · cited by 5Matrix.cons_fin_oneOrientation.areaForm_apply_self · cited by 5Orientation.areaForm_appl…Subgroup.strictPeriods_eq_zmultiples_one_of_T_mem · cited by 4Subgroup.strictPeriods_eq…MvPowerSeries.HasSubst.X_X · cited by 4HasSubst.X_XMvPowerSeries.HasSubst.X_zero · cited by 4HasSubst.X_zeroMvPowerSeries.HasSubst.zero_X · cited by 4HasSubst.zero_XOnePoint.smul_infty_eq_ite · cited by 4OnePoint.smul_infty_eq_iteMatrix.vecCons · cited by 852Matrix.vecConsMatrix.cons_val_fin_oneCITED BYCITES

Cites1

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

Cited by225

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 225.