Library ▹ Essentials ▹ Numbers ▹ Cardinal numbers
Definition 1.8.2.13.  Let κ, μ be cardinal numbers. We define
κ ⋅ μ
by:
|K| ⋅ |J| := |K × J|  (K is a set, J is a set)
References.
  • https://en.wikipedia.org/wiki/Cardinal_number#Cardinal_multiplication
  • https://mathworld.wolfram.com/CardinalMultiplication.html
  • https://proofwiki.org/wiki/Definition:Product_of_Cardinals
  • https://leanprover-community.github.io/mathlib_docs/set_theory/cardinal.html#cardinal.mul_def
[View Source]