Mathlib v3 is deprecated. Go to Mathlib v4

Theorem cardinal.mk_sum

Modification history

2021-10-31 17:26

src/set_theory/cardinal.lean

refactor(set_theory/cardinal): swap sides of `simp` lemmas (#10040) …

Added cardinal.mk_sum View on Github →