Theorems · Theorem · logic and foundations
Cardinal.mk_finsupp_lift_of_fintype
∀ (α : Type u) (β : Type v) [inst : Fintype α] [inst_1 : Zero β],
Cardinal.mk (α →₀ β) = Cardinal.lift.{u, v} (Cardinal.mk β) ^ Fintype.card α- Defined in
- Mathlib.SetTheory.Cardinal.Finsupp
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fintypestatement and proof · cited by 7,736
- Finsuppstatement and proof · cited by 5,255
- Cardinalstatement · cited by 2,598
- Fintype.cardstatement and proof · cited by 1,386
- Cardinal.mkstatement and proof · cited by 942
- Cardinal.liftstatement and proof · cited by 583
- Cardinal.mk_fintypeproof · cited by 81
- Finsupp.equivFunOnFiniteproof · cited by 50
- Cardinal.lift_natCastproof · cited by 39
- Equiv.cardinal_eqproof · cited by 35
- Cardinal.mk_piproof · cited by 11
- Cardinal.prod_constproof · cited by 8
Cited by4
Results whose statement or proof uses this declaration.
- Cardinal.mk_finsupp_lift_of_infinite'proof · cited by 7
- MonoidAlgebra.cardinalMk_eq_lift_of_fintypeproof · cited by 3
- AddMonoidAlgebra.cardinalMk_eq_lift_of_fintypeproof · cited by 2
- Cardinal.mk_finsupp_of_fintypeproof · cited by 1