Theorems · Theorem · combinatorics
Fin.revPerm_apply
∀ {n : ℕ} (i : Fin n), Fin.revPerm i = i.rev- Defined in
- Mathlib.Data.Fin.Rev
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 22 from the axioms · uses propext, Quot.sound
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.
- DFunLike.coestatement and proof · cited by 62,936
- Equivstatement · cited by 8,337
- Fin.revPermstatement and proof · cited by 25
Cited by15
Results whose statement or proof uses this declaration.
- isSymmSndFDerivWithinAt_iff_iteratedFDerivWithinproof · cited by 3
- Polynomial.quo_add_sum_rem_mul_pow_inverse_uniqueproof · cited by 1
- IsSymmSndFDerivWithinAt.iteratedFDerivWithin_consproof · cited by 1
- Polynomial.mul_prod_pow_inverse_eq_quo_add_sum_rem_mul_pow_inverseproof · cited by 1
- LinearMap.IsSymmetric.card_filter_eigenvalues_eqproof · cited by 1
- LinearMap.IsSymmetric.exists_eigenvalues_eqproof · cited by 1
- Fin.map_revPerm_Iccproof · cited by 0
- Fin.map_revPerm_Iciproof · cited by 0
- Fin.map_revPerm_Icoproof · cited by 0
- Fin.map_revPerm_Iicproof · cited by 0
- Fin.map_revPerm_Iioproof · cited by 0
- Fin.map_revPerm_Iocproof · cited by 0