Theorems · Theorem · logic and foundations
Cardinal.mul_eq_max_of_aleph0_le_left
∀ {a b : Cardinal.{u_1}}, Cardinal.aleph0 ≤ a → b ≠ 0 → a * b = max a b- Defined in
- Mathlib.SetTheory.Cardinal.Arithmetic
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 102 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.
- mul_oneproof · cited by 3,885
- LE.le.transproof · cited by 3,151
- Cardinalstatement and proof · cited by 2,598
- LT.lt.leproof · cited by 2,189
- Cardinal.aleph0statement and proof · cited by 521
- LE.le.antisymmproof · cited by 507
- le_or_gtproof · cited by 269
- max_eq_leftproof · cited by 96
- mul_le_mul_rightproof · cited by 47
- Cardinal.one_le_iff_ne_zeroproof · cited by 14
- Cardinal.mul_eq_maxproof · cited by 8
- Cardinal.mul_le_max_of_aleph0_le_leftproof · cited by 3
Cited by8
Results whose statement or proof uses this declaration.
- Cardinal.mul_eq_leftproof · cited by 8
- Cardinal.mk_finsupp_lift_of_infiniteproof · cited by 6
- Cardinal.ciSup_mulproof · cited by 2
- Cardinal.mul_eq_max_of_aleph0_le_rightproof · cited by 2
- FirstOrder.Language.Term.card_sigmaproof · cited by 1
- Cardinal.mul_eq_max'proof · cited by 1
- Cardinal.mul_le_maxproof · cited by 1
- Cardinal.mul_eq_left_iffproof · cited by 0