Commit 2025-04-28 13:10 0550cf4a

View on Github →

chore(Cardinal): rename mk_pNat -> mk_pnat (#24429)

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Basic.lean

deleted theorem Cardinal.mk_pNat

added theorem Cardinal.mk_pnat