Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-30 13:16 1331e29b

View on Github →

chore(*): completing most of the -T50000 challenge (#2281)

Estimated changes

Modified src/analysis/complex/basic.lean

Modified src/analysis/normed_space/real_inner_product.lean

Modified src/category_theory/limits/over.lean

Modified src/measure_theory/integration.lean

Modified src/measure_theory/simple_func_dense.lean

Modified src/ring_theory/fractional_ideal.lean

added theorem ring.fractional_ideal.ne_zero_of_mul_eq_one

Modified src/topology/algebra/infinite_sum.lean

Modified src/topology/category/Top/adjunctions.lean

Modified src/topology/category/UniformSpace.lean