Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-27 08:41 57ac39bd

View on Github →

chore(data/real/ennreal): drop some lemmas (#18501) Drop lemmas that are in fact more general lemmas applied to ennreal. For now, these lemmas are marked as @[deprecated] in leanprover-community/mathlib4#2388.

Estimated changes

deleted theorem ennreal.add_top
modified theorem ennreal.bit0_top
modified theorem ennreal.coe_lt_coe_nat
modified theorem ennreal.coe_nat_lt_coe
deleted theorem ennreal.coe_nat_mono
deleted theorem ennreal.coe_nonneg
deleted theorem ennreal.mul_le_mul
modified theorem ennreal.mul_left_mono
modified theorem ennreal.mul_right_mono
deleted theorem ennreal.pow_le_pow
deleted theorem ennreal.top_add
deleted theorem ennreal.two_ne_zero
deleted theorem ennreal.zero_lt_two
modified theorem ennreal.nhds_zero