Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-20 08:19 a6d5ba81

View on Github →

chore(set_theory/cardinal): add map, induction_on etc (#9812)

Estimated changes

added theorem cardinal.induction_on
modified theorem cardinal.lift_id'
modified theorem cardinal.lift_id
modified theorem cardinal.lift_umax
modified theorem cardinal.lift_zero
added def cardinal.map
added theorem cardinal.map_mk
added def cardinal.map₂
added theorem cardinal.mk_congr
modified theorem cardinal.succ_ne_zero