Theorems · Theorem · logic and foundations
Cardinal.mul_eq_left
∀ {a b : Cardinal.{u_1}}, Cardinal.aleph0 ≤ a → b ≤ a → b ≠ 0 → a * b = a- Defined in
- Mathlib.SetTheory.Cardinal.Arithmetic
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 103 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- Cardinalstatement and proof · cited by 2,598
- Cardinal.aleph0statement and proof · cited by 521
- max_eq_leftproof · cited by 96
- Cardinal.mul_eq_max_of_aleph0_le_leftproof · cited by 8
Cited by8
Results whose statement or proof uses this declaration.
- Cardinal.continuum_power_aleph0proof · cited by 2
- Cardinal.mul_eq_rightproof · cited by 2
- WType.cardinalMk_le_max_aleph0_of_finite'proof · cited by 2
- Cardinal.continuum_mul_aleph0proof · cited by 1
- Cardinal.continuum_mul_selfproof · cited by 1
- IsTranscendenceBasis.lift_rank_eq_max_liftproof · cited by 1
- Cardinal.mk_freeAddGroupproof · cited by 0
- Cardinal.mk_freeGroupproof · cited by 0