Theorems · Theorem · combinatorics
Finite.of_equiv
∀ {β : Sort u_2} (α : Sort u_3) [h : Finite α] (f : α ≃ β), Finite β- Defined in
- Mathlib.Data.Finite.Defs
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses Quot.sound
- Assumes
- Finite
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.
- Equivstatement and proof · cited by 8,337
- Equiv.symmproof · cited by 3,681
- Finitestatement and proof · cited by 3,029
- Equiv.transproof · cited by 337
Cited by20
Results whose statement or proof uses this declaration.
- Finite.of_injectiveproof · cited by 32
- Equiv.finite_iffproof · cited by 21
- nonempty_sections_of_finite_cofiltered_systemproof · cited by 4
- Submodule.finiteQuotientOfFreeOfRankEqproof · cited by 3
- CommGroup.finite_of_fg_isMulTorsionproof · cited by 2
- Ring.HasFiniteQuotients.finite_setOfPred_memproof · cited by 2
- Projectivization.finite_iff_of_finiteproof · cited by 2
- Valued.integer.finite_quotient_maximalIdeal_pow_of_finite_residueFieldproof · cited by 1
- Set.Finite.induction_toproof · cited by 1
- Module.finite_of_fg_torsionproof · cited by 1
- IsPGroup.card_orbitproof · cited by 1
- ConnectedComponents.exists_fun_isClopen_of_infiniteproof · cited by 1