Commit 2022-12-08 07:28 51eda27a

View on Github →

feat: port Algebra.Order.[Ring|Field].Defs (#905) 655994e298904d7e5bbd1e18c95defd7b543eb94 Ports:

Algebra.Order.Ring.Defs
Algebra.Order.Ring.Canonical
Algebra.Order.Ring.CharZero
Algebra.Order.Field.Defs Todo:
Fix a few proofs; nothing looks bad.
Deal with unused arguments.
Check #aligns
Fix casing of names in comments.
Long lines
Linting
Remove old Algebra.Order.Ring

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Basic.lean

added theorem bit0_add

added theorem bit0_zero

added theorem bit1_add'

added theorem bit1_add

added theorem bit1_zero

Modified Mathlib/Algebra/Group/Defs.lean

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

Deleted Mathlib/Algebra/Order/Ring.lean

Created Mathlib/Algebra/Order/Ring/Canonical.lean

added theorem CanonicallyOrderedCommSemiring.mul_pos

added theorem mul_add_mul_le_mul_add_mul'

added theorem mul_add_mul_le_mul_add_mul

added theorem mul_add_mul_lt_mul_add_mul'

added theorem mul_add_mul_lt_mul_add_mul

added theorem mul_tsub

added theorem tsub_mul

Created Mathlib/Algebra/Order/Ring/CharZero.lean

Created Mathlib/Algebra/Order/Ring/Defs.lean

added theorem Antitone.const_mul

added theorem Antitone.const_mul_of_nonpos

added theorem Antitone.mul

added theorem Antitone.mul_const

added theorem Antitone.mul_const_of_nonpos

added theorem Antitone.mul_monotone

added theorem Monotone.const_mul

added theorem Monotone.const_mul_of_nonpos

added theorem Monotone.mul

added theorem Monotone.mul_antitone

added theorem Monotone.mul_const

added theorem Monotone.mul_const_of_nonpos

added theorem Monotone.mul_strict_mono

added theorem StrictAnti.const_mul

added theorem StrictAnti.const_mul_of_neg

added theorem StrictAnti.mul_const

added theorem StrictAnti.mul_const_of_neg

added theorem StrictMono.const_mul

added theorem StrictMono.const_mul_of_neg

added theorem StrictMono.mul

added theorem StrictMono.mul_const

added theorem StrictMono.mul_const_of_neg

added theorem StrictMono.mul_monotone

added def StrictOrderedCommRing.toOrderedCommRing'

added def StrictOrderedCommSemiring.toOrderedCommSemiring'

added def StrictOrderedRing.toOrderedRing'

added def StrictOrderedSemiring.toOrderedSemiring'

added theorem Units.inv_neg

added theorem Units.inv_pos

added theorem add_le_mul'

added theorem add_le_mul

added theorem add_le_mul_of_left_le_right

added theorem add_le_mul_of_right_le_left

added theorem add_le_mul_two_add

added theorem add_one_le_two_mul

added theorem antitone_mul_left

added theorem antitone_mul_right

added theorem bit0_le_bit0

added theorem bit0_lt_bit0

added theorem bit1_le_bit1

added theorem bit1_lt_bit1

added theorem bit1_mono

added theorem bit1_pos'

added theorem bit1_pos

added theorem cmp_mul_neg_left

added theorem cmp_mul_neg_right

added theorem cmp_mul_pos_left

added theorem cmp_mul_pos_right

added theorem eq_zero_of_mul_self_add_mul_self_eq_zero

added theorem le_iff_exists_nonneg_add

added theorem le_neg_self_iff

added theorem le_of_mul_le_of_one_le

added theorem lt_mul_left

added theorem lt_mul_right

added theorem lt_mul_self

added theorem lt_neg_self_iff

added theorem lt_of_mul_lt_mul_of_nonpos_left

added theorem lt_of_mul_lt_mul_of_nonpos_right

added theorem lt_two_mul_self

added theorem max_mul_mul_le_max_mul_max

added theorem max_mul_of_nonneg

added theorem min_mul_of_nonneg

added theorem monotone_mul_left_of_nonneg

added theorem monotone_mul_right_of_nonneg

added theorem mul_le_mul_left_of_neg

added theorem mul_le_mul_of_nonneg_of_nonpos'

added theorem mul_le_mul_of_nonneg_of_nonpos

added theorem mul_le_mul_of_nonpos_left

added theorem mul_le_mul_of_nonpos_of_nonneg'

added theorem mul_le_mul_of_nonpos_of_nonneg

added theorem mul_le_mul_of_nonpos_of_nonpos'

added theorem mul_le_mul_of_nonpos_of_nonpos

added theorem mul_le_mul_of_nonpos_right

added theorem mul_le_mul_right_of_neg

added theorem mul_le_one

added theorem mul_lt_mul''

added theorem mul_lt_mul'

added theorem mul_lt_mul

added theorem mul_lt_mul_left_of_neg

added theorem mul_lt_mul_of_neg_left

added theorem mul_lt_mul_of_neg_right

added theorem mul_lt_mul_right_of_neg

added theorem mul_lt_one_of_nonneg_of_lt_one_left

added theorem mul_lt_one_of_nonneg_of_lt_one_right

added theorem mul_max_of_nonneg

added theorem mul_min_of_nonneg

added theorem mul_neg_iff

added theorem mul_nonneg_iff

added theorem mul_nonneg_iff_left_nonneg_of_pos

added theorem mul_nonneg_iff_right_nonneg_of_pos

added theorem mul_nonneg_of_nonpos_of_nonpos

added theorem mul_nonneg_of_three

added theorem mul_nonpos_iff

added theorem mul_pos_iff

added theorem mul_pos_of_neg_of_neg

added theorem mul_self_add_mul_self_eq_zero

added theorem mul_self_inj

added theorem mul_self_le_mul_self_iff

added theorem mul_self_le_mul_self_of_le_of_neg_le

added theorem mul_self_lt_mul_self

added theorem mul_self_lt_mul_self_iff

added theorem mul_self_nonneg

added theorem mul_self_pos

added theorem neg_iff_pos_of_mul_neg

added theorem neg_le_self_iff

added theorem neg_lt_self_iff

added theorem neg_of_mul_neg_left

added theorem neg_of_mul_neg_right

added theorem neg_one_lt_zero

added theorem nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nnonneg

added theorem nonneg_le_nonneg_of_sq_le_sq

added theorem nonneg_of_mul_nonneg_left

added theorem nonneg_of_mul_nonneg_right

added theorem nonneg_of_mul_nonpos_left

added theorem nonneg_of_mul_nonpos_right

added theorem nonpos_of_mul_nonneg_left

added theorem nonpos_of_mul_nonneg_right

added theorem nonpos_of_mul_nonpos_left

added theorem nonpos_of_mul_nonpos_right

added theorem one_le_bit1

added theorem one_le_mul_of_one_le_of_one_le

added theorem one_lt_bit1

added theorem one_lt_mul_of_le_of_lt

added theorem one_lt_mul_of_lt_of_le

added theorem pos_iff_neg_of_mul_neg

added theorem pos_of_mul_neg_left

added theorem pos_of_mul_neg_right

added theorem pow_nonneg

added theorem pow_pos

added theorem strict_anti_mul_left

added theorem strict_anti_mul_right

added theorem strict_mono_mul_left_of_pos

added theorem strict_mono_mul_right_of_pos

added theorem strict_mono_on_mul_self

added theorem sub_one_lt

added theorem zero_le_bit0

added theorem zero_le_mul_left

added theorem zero_le_mul_right

added theorem zero_lt_bit0

Modified Mathlib/Algebra/Order/ZeroLEOne.lean

Modified Mathlib/Data/Int/Basic.lean

Modified Mathlib/Data/Int/Order/Basic.lean

Modified Mathlib/Data/Rat/Order.lean

Modified Mathlib/Tactic/Linarith/Lemmas.lean

deleted theorem mul_nonneg_of_nonpos_of_nonpos

deleted theorem mul_pos_of_neg_of_neg

deleted theorem mul_self_nonneg

deleted theorem zero_lt_one''

Modified Mathlib/Tactic/Linarith/Verification.lean

Modified Mathlib/Tactic/Positivity/Basic.lean

deleted theorem pow_nonneg

deleted theorem pow_pos

Modified Mathlib/Tactic/Zify.lean

modified theorem Mathlib.Tactic.Zify.nat_cast_ne

Modified test/nontriviality.lean

deleted theorem zero_le_one

deleted theorem zero_le_two