Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-01 21:26 8aa23326

View on Github →

chore(*): golf some proofs (#5548) Parts of #5539

Estimated changes

Modified src/algebra/big_operators/ring.lean

Modified src/algebra/group_power/basic.lean

Modified src/algebra/ordered_ring.lean

Modified src/analysis/complex/polynomial.lean

Modified src/analysis/convex/basic.lean

Modified src/analysis/hofer.lean

Modified src/data/rat/cast.lean

Modified src/data/real/ennreal.lean

modified theorem ennreal.add_eq_top

modified theorem ennreal.add_lt_top

added theorem ennreal.mul_lt_mul

Modified src/field_theory/adjoin.lean

Modified src/topology/instances/ennreal.lean