Theorems · Theorem · logic and foundations
Cardinal.toNat_lift
∀ (c : Cardinal.{v}), Cardinal.toNat (Cardinal.lift.{u, v} c) = Cardinal.toNat c- Defined in
- Mathlib.SetTheory.Cardinal.ToNat
- Cited by
- 41 results in Mathlib
- Foundations
- Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
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
- Cardinalstatement and proof · cited by 2,598
- MonoidWithZeroHomstatement · cited by 704
- Cardinal.liftstatement · cited by 583
- Cardinal.toNatstatement · cited by 153
- ENat.toNatproof · cited by 143
- Cardinal.toENatproof · cited by 92
- Cardinal.toENat_liftproof · cited by 10
Cited by41
Results whose statement or proof uses this declaration.
- LinearEquiv.finrank_eqproof · cited by 65
- Module.finrank_mul_finrankproof · cited by 26
- Nat.card_prodproof · cited by 24
- Nat.card_le_card_of_injectiveproof · cited by 19
- Nat.card_le_card_of_surjectiveproof · cited by 11
- Nat.card_piproof · cited by 10
- Algebra.finrank_eq_of_equiv_equivproof · cited by 7
- Module.finrank_le_finrank_of_rank_le_rankproof · cited by 7
- Module.finrank_tensorProductproof · cited by 6
- Module.finrank_eq_nat_card_basisproof · cited by 5
- Module.finrank_prodproof · cited by 4
- Module.finrank_finsupp_selfproof · cited by 3