Theorems · Theorem · group theory
Matrix.zero_empty
∀ {α : Type u_1} [inst : Zero α], 0 = ![]- Defined in
- Mathlib.Algebra.Group.Fin.Tuple
- Cited by
- 34 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses Quot.sound
- Assumes
- Zero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Matrix.vecEmptystatement · cited by 832
- Matrix.empty_eqproof · cited by 20
Cited by34
Results whose statement or proof uses this declaration.
- ContDiffWithinAt.compproof · cited by 18
- Orientation.areaForm_to_volumeFormproof · cited by 8
- hasFTaylorSeriesUpToOn_univ_iffproof · cited by 8
- Height.mulHeight₁_eq_mulHeightproof · cited by 6
- contDiffOn_zeroproof · cited by 5
- Matrix.finZeroElim_eq_zeroproof · cited by 5
- ContinuousMultilinearMap.fin0_apply_normproof · cited by 3
- isSymmSndFDerivWithinAt_iff_iteratedFDerivWithinproof · cited by 3
- FormalMultilinearSeries.div_le_radius_compContinuousLinearMapproof · cited by 3
- compContinuousLinearMap_zeroproof · cited by 2
- Topology.RelCWComplex.cellFrontier_zero_eq_emptyproof · cited by 2
- FormalMultilinearSeries.derivSeries_apply_diagproof · cited by 2