Commit 2020-09-28 11:21 ad680c24

View on Github →

chore(algebra/ordered_ring): remove duplicate lemma (#4295) ordered_ring.two_pos and ordered_ring.zero_lt_two had ended up identical. I kept zero_lt_two.

Estimated changes

Modified src/algebra/gcd_monoid.lean

Modified src/algebra/ordered_field.lean

modified theorem half_pos

Modified src/algebra/ordered_ring.lean

deleted theorem four_pos

deleted theorem two_pos

added theorem zero_lt_four

modified theorem zero_lt_two

Modified src/analysis/hofer.lean

Modified src/analysis/normed_space/basic.lean

modified theorem real.norm_two

Modified src/analysis/normed_space/finite_dimension.lean

Modified src/analysis/special_functions/trigonometric.lean

Modified src/analysis/specific_limits.lean

Modified src/data/complex/basic.lean

Modified src/data/complex/is_R_or_C.lean

Modified src/data/real/basic.lean

Modified src/data/real/ennreal.lean

modified theorem ennreal.two_ne_zero

deleted theorem ennreal.two_pos

added theorem ennreal.zero_lt_two

Modified src/data/real/hyperreal.lean

Modified src/data/real/pi.lean

Modified src/number_theory/pythagorean_triples.lean

Modified src/topology/algebra/ordered.lean

Modified src/topology/metric_space/basic.lean

Modified src/topology/uniform_space/absolute_value.lean