Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-21 11:25 edd801f7

View on Github →

chore(set_theory/cardinal): ensure c ^ ↑n = c ^ n is definitional (#9842)

Estimated changes

modified theorem cardinal.pow_cast_right