Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-05-27 18:15 f563ac80

View on Github →

chore(data/pnat): remove nat -> pnat coercion

Estimated changes

Modified analysis/real.lean

Modified data/finset.lean

deleted theorem finset.max_eq_inf_with_top

added theorem finset.min_eq_inf_with_top

Modified data/pnat.lean

deleted theorem pnat.coe_nat_coe

added theorem pnat.coe_to_pnat'

deleted theorem pnat.nat_coe_coe