Theorems · Definition · order theory
finCongr
{n m : ℕ} → n = m → Fin n ≃ Fin mThe 'identity' equivalence between Fin m and Fin n when m = n.
- Defined in
- Mathlib.Data.Fin.SuccPred
- Cited by
- 78 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equivstatement · cited by 8,337
- Fin.rightInverse_castproof · cited by 3
- Fin.leftInverse_castproof · cited by 0
Cited by97
Results whose statement or proof uses this declaration.
- finCongr_applystatement and proof · cited by 47
- finRotateproof · cited by 36
- TensorPower.castproof · cited by 14
- Fin.natAdd_castLEEmbproof · cited by 11
- Polynomial.resultant_commproof · cited by 11
- ZMod.ringEquivCongrproof · cited by 11
- MvPolynomial.universalFactorizationMapPresentationproof · cited by 10
- FormalMultilinearSeries.changeOriginIndexEquivproof · cited by 9
- WeierstrassCurve.Affine.CoordinateRing.basisproof · cited by 8
- Orientation.finOrthonormalBasisproof · cited by 8
- OrthonormalBasis.fromOrthogonalSpanSingletonproof · cited by 8
- Module.finBasisOfFinrankEqproof · cited by 6