Theorems · Definition · combinatorics
Fin.revPerm
{n : ℕ} → Equiv.Perm (Fin n)Fin.rev as an Equiv.Perm, the antitone involution Fin n → Fin n given by
i ↦ n-(i+1).
- Defined in
- Mathlib.Data.Fin.Rev
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 21 from the axioms · uses propext
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.
- Equiv.Permstatement · cited by 1,375
- Function.Involutive.toPermproof · cited by 16
- Fin.rev_involutiveproof · cited by 3
Cited by26
Results whose statement or proof uses this declaration.
- Fin.revPerm_applystatement and proof · cited by 15
- Fin.revOrderIsoproof · cited by 11
- LinearMap.IsSymmetric.eigenvalues_defstatement and proof · cited by 4
- isSymmSndFDerivWithinAt_iff_iteratedFDerivWithinstatement and proof · cited by 3
- LinearMap.IsSymmetric.eigenvalues_antitoneproof · cited by 3
- LinearMap.IsSymmetric.hasEigenvector_eigenvectorBasisproof · cited by 2
- Polynomial.mul_prod_pow_inverse_eq_quo_add_sum_rem_mul_pow_inverseproof · cited by 1
- IsSymmSndFDerivWithinAt.iteratedFDerivWithin_consproof · cited by 1
- LinearMap.IsSymmetric.card_filter_eigenvalues_eqproof · cited by 1
- Polynomial.quo_add_sum_rem_mul_pow_inverse_uniqueproof · cited by 1
- Fin.image_revproof · cited by 1
- LinearMap.IsSymmetric.eigenvectorBasis_defstatement and proof · cited by 1