Commit 2024-07-01 15:55 9bfe41c4

View on Github →

chore(Data/Real/EReal): theorems to lemmas (#14324) This PR turns some theorems into lemmas as suggested here.

Estimated changes

Modified Mathlib/Data/Real/EReal.lean

modified theorem EReal.add_sub_cancel_right

modified theorem EReal.antitone_div_right_of_nonpos

modified theorem EReal.bot_div_of_neg_ne_bot

modified theorem EReal.bot_div_of_pos_ne_top

modified theorem EReal.bot_mul_bot

modified theorem EReal.bot_mul_coe_of_neg

modified theorem EReal.bot_mul_coe_of_pos

modified theorem EReal.bot_mul_of_neg

modified theorem EReal.bot_mul_of_pos

modified theorem EReal.bot_mul_top

modified theorem EReal.coe_div

modified theorem EReal.coe_inv

modified theorem EReal.coe_mul_bot_of_neg

modified theorem EReal.coe_mul_bot_of_pos

modified theorem EReal.coe_mul_top_of_neg

modified theorem EReal.coe_mul_top_of_pos

modified theorem EReal.div_bot

modified theorem EReal.div_div

modified theorem EReal.div_eq_inv_mul

modified theorem EReal.div_le_div_right_of_nonneg

modified theorem EReal.div_le_div_right_of_nonpos

modified theorem EReal.div_le_iff_le_mul

modified theorem EReal.div_lt_div_right_of_neg

modified theorem EReal.div_lt_div_right_of_pos

modified theorem EReal.div_mul_cancel

modified theorem EReal.div_nonneg

modified theorem EReal.div_nonneg_of_nonpos_of_nonpos

modified theorem EReal.div_nonpos_of_nonneg_of_nonpos

modified theorem EReal.div_nonpos_of_nonpos_of_nonneg

modified theorem EReal.div_right_distrib_of_nonneg

modified theorem EReal.div_self

modified theorem EReal.div_top

modified theorem EReal.div_zero

modified theorem EReal.induction₂_neg_left

modified theorem EReal.induction₂_symm_neg

modified theorem EReal.inv_bot

modified theorem EReal.inv_inv

modified theorem EReal.inv_neg

modified theorem EReal.inv_neg_of_neg_ne_bot

modified theorem EReal.inv_nonneg_of_nonneg

modified theorem EReal.inv_nonpos_of_nonpos

modified theorem EReal.inv_pos_of_pos_ne_top

modified theorem EReal.inv_top

modified theorem EReal.inv_zero

modified theorem EReal.le_div_iff_mul_le

modified theorem EReal.le_iff_le_forall_real_gt

modified theorem EReal.left_distrib_of_nonneg

modified theorem EReal.monotone_div_right_of_nonneg

modified theorem EReal.mul_bot_of_neg

modified theorem EReal.mul_bot_of_pos

modified theorem EReal.mul_div

modified theorem EReal.mul_div_cancel

modified theorem EReal.mul_div_mul_cancel

modified theorem EReal.mul_div_right

modified theorem EReal.mul_inv

modified theorem EReal.mul_pos

modified theorem EReal.mul_top_of_neg

modified theorem EReal.mul_top_of_pos

modified theorem EReal.right_distrib_of_nonneg

modified theorem EReal.sign_mul_inv_abs'

modified theorem EReal.sign_mul_inv_abs

modified theorem EReal.strictAnti_div_right_of_neg

modified theorem EReal.strictMono_div_right_of_pos

modified theorem EReal.toReal_mul

modified theorem EReal.top_div_of_neg_ne_bot

modified theorem EReal.top_div_of_pos_ne_top

modified theorem EReal.top_mul_bot

modified theorem EReal.top_mul_coe_of_neg

modified theorem EReal.top_mul_coe_of_pos

modified theorem EReal.top_mul_of_neg

modified theorem EReal.top_mul_of_pos

modified theorem EReal.top_mul_top

modified theorem EReal.zero_div