Theorems · Theorem · logic and foundations
Cardinal.mk_prod
∀ (α : Type u) (β : Type v),
Cardinal.mk (α × β) = Cardinal.lift.{v, u} (Cardinal.mk α) * Cardinal.lift.{u, v} (Cardinal.mk β)- Defined in
- Mathlib.SetTheory.Cardinal.Defs
- Cited by
- 19 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.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equiv.symmproof · cited by 3,681
- Cardinalstatement · cited by 2,598
- Cardinal.mkstatement · cited by 942
- Cardinal.liftstatement · cited by 583
- Equiv.uliftproof · cited by 115
- Cardinal.mk_congrproof · cited by 55
- Equiv.prodCongrproof · cited by 24
Cited by19
Results whose statement or proof uses this declaration.
- Nat.card_prodproof · cited by 24
- Cardinal.mk_finsupp_lift_of_infiniteproof · cited by 6
- lift_rank_mul_lift_rankproof · cited by 4
- rank_tensorProductproof · cited by 4
- rank_matrix_moduleproof · cited by 3
- Cardinal.mk_quaternionAlgebraproof · cited by 3
- ENat.card_prodproof · cited by 2
- Cardinal.mk_perm_eq_self_powerproof · cited by 2
- Cardinal.mk_complexproof · cited by 2
- Field.Emb.cardinal_separableClosureproof · cited by 2
- Cardinal.prod_eq_of_fintypeproof · cited by 2
- AddOreLocalization.cardinalMk_le_maxproof · cited by 1