Theorems · Theorem · order theory
Fin.castPred_one
∀ {n : ℕ} [inst : NeZero n], Fin.castPred 1 ⋯ = 1- Defined in
- Mathlib.Data.Fin.SuccPred
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 28 from the axioms · uses propext
- Assumes
- NeZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- LT.lt.nestatement and proof · cited by 872
- Iff.notstatement and proof · cited by 489
- Fin.castPredstatement and proof · cited by 89
- Fin.one_lt_laststatement and proof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- FirstOrder.Field.FieldAxiom.realize_toSentence_iff_toPropproof · cited by 1