Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-10 13:41 11c2b8c1

View on Github →

chore(data/real/ennreal): Protect ambiguous lemmas (#18076) Protect ennreal.X if declaration X already exists.

Estimated changes

deleted theorem ennreal.add_div
deleted theorem ennreal.add_halves
deleted theorem ennreal.div_add_div_same
deleted theorem ennreal.div_eq_div_iff
deleted theorem ennreal.div_le_div
deleted theorem ennreal.div_le_iff_le_mul
deleted theorem ennreal.div_mul_cancel
deleted theorem ennreal.div_self
deleted theorem ennreal.half_le_self
deleted theorem ennreal.half_lt_self
deleted theorem ennreal.half_pos
deleted theorem ennreal.inv_eq_zero
deleted theorem ennreal.inv_le_inv
deleted theorem ennreal.inv_le_one
deleted theorem ennreal.inv_lt_inv
deleted theorem ennreal.inv_lt_one
deleted theorem ennreal.inv_mul_cancel
deleted theorem ennreal.inv_ne_zero
deleted theorem ennreal.inv_pos
deleted theorem ennreal.le_div_iff_mul_le
deleted theorem ennreal.lt_div_iff_mul_lt
deleted theorem ennreal.mul_div_cancel'
deleted theorem ennreal.mul_inv
deleted theorem ennreal.mul_inv_cancel
deleted theorem ennreal.one_half_lt_one
deleted theorem ennreal.one_le_inv
deleted theorem ennreal.zero_div
deleted theorem ennreal.zpow_add