Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-19 11:39 4140f789

View on Github →

feat(algebra/ordered_semiring): relax 0 < 1 to 0 ≤ 1 (#4363) Per discussion in #4296.

Estimated changes

Modified archive/imo/imo1972_b2.lean

Modified src/algebra/group_power/basic.lean

Modified src/algebra/linear_ordered_comm_group_with_zero.lean

deleted theorem zero_lt_one'

Modified src/algebra/ordered_field.lean

Modified src/algebra/ordered_ring.lean

modified theorem canonically_ordered_semiring.zero_lt_one

modified theorem le_of_mul_le_of_one_le

modified def nonneg_ring.to_linear_nonneg_ring

deleted def nonneg_ring.to_ordered_ring

added theorem zero_le_two

added theorem zero_lt_one'

modified theorem zero_lt_one

Modified src/algebra/punit_instances.lean

Modified src/analysis/normed_space/basic.lean

modified theorem real.norm_two

Modified src/analysis/normed_space/mazur_ulam.lean

Modified src/analysis/special_functions/pow.lean

Modified src/analysis/special_functions/trigonometric.lean

Modified src/data/complex/basic.lean

Modified src/data/complex/is_R_or_C.lean

Modified src/data/int/basic.lean

Modified src/data/nat/basic.lean

Modified src/data/num/lemmas.lean

Modified src/data/polynomial/div.lean

Modified src/data/rat/order.lean

Modified src/data/real/basic.lean

Modified src/data/real/ennreal.lean

modified theorem ennreal.one_lt_two

Modified src/data/real/nnreal.lean

Modified src/data/zsqrtd/basic.lean

Modified src/dynamics/circle/rotation_number/translation_number.lean

Modified src/order/filter/filter_product.lean

added theorem filter.germ.le_def

Modified src/ring_theory/subsemiring.lean

Modified src/tactic/linarith/verification.lean

Modified src/tactic/norm_num.lean

Modified src/tactic/omega/coeffs.lean

Modified src/topology/algebra/floor_ring.lean

Modified src/topology/metric_space/basic.lean

Modified src/topology/path_connected.lean