Commit 2022-12-19 23:36 172b8503

View on Github →

feat: port Algebra.Order.Field.Basic (#1065)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/Field/Basic.lean

added theorem IsGLB.mul_left

added theorem IsGLB.mul_right

added theorem IsLUB.mul_left

added theorem IsLUB.mul_right

added theorem Monotone.div_const

added def OrderIso.mulLeft₀

added def OrderIso.mulRight₀

added theorem StrictMono.div_const

added theorem abs_div

added theorem abs_inv

added theorem abs_one_div

added theorem add_div_two_lt_right

added theorem add_halves

added theorem add_self_div_two

added theorem add_sub_div_two_lt

added theorem div_le_div

added theorem div_le_div_iff

added theorem div_le_div_left

added theorem div_le_div_of_le

added theorem div_le_div_of_le_left

added theorem div_le_div_of_le_of_nonneg

added theorem div_le_div_of_nonpos_of_le

added theorem div_le_div_right

added theorem div_le_div_right_of_neg

added theorem div_le_iff'

added theorem div_le_iff

added theorem div_le_iff_of_neg'

added theorem div_le_iff_of_neg

added theorem div_le_of_nonneg_of_le_mul

added theorem div_le_one

added theorem div_le_one_iff

added theorem div_le_one_of_le

added theorem div_le_one_of_neg

added theorem div_le_self

added theorem div_lt_div'

added theorem div_lt_div

added theorem div_lt_div_iff

added theorem div_lt_div_left

added theorem div_lt_div_of_lt

added theorem div_lt_div_of_lt_left

added theorem div_lt_div_of_neg_of_lt

added theorem div_lt_div_right

added theorem div_lt_div_right_of_neg

added theorem div_lt_iff'

added theorem div_lt_iff

added theorem div_lt_iff_of_neg'

added theorem div_lt_iff_of_neg

added theorem div_lt_one

added theorem div_lt_one_iff

added theorem div_lt_one_of_neg

added theorem div_lt_self

added theorem div_mul_le_div_mul_of_div_le_div

added theorem div_neg_iff

added theorem div_neg_of_neg_of_pos

added theorem div_neg_of_pos_of_neg

added theorem div_nonneg

added theorem div_nonneg_iff

added theorem div_nonneg_of_nonpos

added theorem div_nonpos_iff

added theorem div_nonpos_of_nonneg_of_nonpos

added theorem div_nonpos_of_nonpos_of_nonneg

added theorem div_pos

added theorem div_pos_iff

added theorem div_pos_of_neg_of_neg

added theorem div_self_le_one

added theorem div_two_lt_of_pos

added theorem div_two_sub_self

added theorem exists_add_lt_and_pos_of_lt

added theorem exists_pos_mul_lt

added theorem half_le_self

added theorem half_lt_self

added theorem half_pos

added theorem inv_le

added theorem inv_le_inv

added theorem inv_le_inv_of_le

added theorem inv_le_inv_of_neg

added theorem inv_le_of_inv_le

added theorem inv_le_of_neg

added theorem inv_le_one

added theorem inv_le_one_iff

added theorem inv_lt

added theorem inv_lt_inv

added theorem inv_lt_inv_of_lt

added theorem inv_lt_inv_of_neg

added theorem inv_lt_of_inv_lt

added theorem inv_lt_of_neg

added theorem inv_lt_one

added theorem inv_lt_one_iff

added theorem inv_lt_one_iff_of_pos

added theorem inv_lt_zero

added theorem inv_mul_le_iff'

added theorem inv_mul_le_iff

added theorem inv_mul_lt_iff'

added theorem inv_mul_lt_iff

added theorem inv_nonneg

added theorem inv_nonpos

added theorem inv_pos

added theorem inv_pos_le_iff_one_le_mul'

added theorem inv_pos_le_iff_one_le_mul

added theorem inv_pos_lt_iff_one_lt_mul'

added theorem inv_pos_lt_iff_one_lt_mul

added theorem inv_pow_anti

added theorem inv_pow_le_inv_pow_of_le

added theorem inv_pow_lt_inv_pow_of_lt

added theorem inv_pow_strictAnti

added theorem inv_strictAntiOn

added theorem le_div_iff'

added theorem le_div_iff

added theorem le_div_iff_of_neg'

added theorem le_div_iff_of_neg

added theorem le_div_self

added theorem le_inv

added theorem le_inv_of_neg

added theorem le_of_forall_sub_le

added theorem le_of_neg_of_one_div_le_one_div

added theorem le_of_one_div_le_one_div

added theorem le_one_div

added theorem le_one_div_of_neg

added theorem left_lt_add_div_two

added theorem lt_div_iff'

added theorem lt_div_iff

added theorem lt_div_iff_of_neg'

added theorem lt_div_iff_of_neg

added theorem lt_inv

added theorem lt_inv_of_neg

added theorem lt_of_neg_of_one_div_lt_one_div

added theorem lt_of_one_div_lt_one_div

added theorem lt_one_div

added theorem lt_one_div_of_neg

added theorem max_div_div_right

added theorem max_div_div_right_of_nonpos

added theorem min_div_div_right

added theorem min_div_div_right_of_nonpos

added theorem mul_inv_le_iff'

added theorem mul_inv_le_iff

added theorem mul_inv_lt_iff'

added theorem mul_inv_lt_iff

added theorem mul_le_mul_of_mul_div_le

added theorem mul_self_inj_of_nonneg

added theorem mul_sub_mul_div_mul_neg_iff

added theorem mul_sub_mul_div_mul_nonpos_iff

added theorem one_div_le

added theorem one_div_le_neg_one

added theorem one_div_le_of_neg

added theorem one_div_le_one_div

added theorem one_div_le_one_div_of_le

added theorem one_div_le_one_div_of_neg

added theorem one_div_le_one_div_of_neg_of_le

added theorem one_div_lt

added theorem one_div_lt_neg_one

added theorem one_div_lt_of_neg

added theorem one_div_lt_one_div

added theorem one_div_lt_one_div_of_lt

added theorem one_div_lt_one_div_of_neg

added theorem one_div_lt_one_div_of_neg_of_lt

added theorem one_div_neg

added theorem one_div_nonneg

added theorem one_div_nonpos

added theorem one_div_pos

added theorem one_div_pow_anti

added theorem one_div_pow_le_one_div_pow_of_le

added theorem one_div_pow_lt_one_div_pow_of_lt

added theorem one_div_pow_strictAnti

added theorem one_div_strictAntiOn

added theorem one_half_lt_one

added theorem one_half_pos

added theorem one_le_div

added theorem one_le_div_iff

added theorem one_le_div_of_neg

added theorem one_le_inv

added theorem one_le_inv_iff

added theorem one_le_one_div

added theorem one_lt_div

added theorem one_lt_div_iff

added theorem one_lt_div_of_neg

added theorem one_lt_inv

added theorem one_lt_inv_iff

added theorem one_lt_one_div

added theorem pow_minus_two_nonneg

added theorem sub_one_div_inv_le_two

added theorem sub_self_div_two

added theorem two_inv_lt_one

added theorem zpow_nonneg

added theorem zpow_pos_of_pos