Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-11 12:46 c7d870e8

View on Github →

chore(compatibility): compatibility with Lean 3.5.0c (#1007)

Estimated changes

Modified src/algebra/ring.lean

added def has_div_of_division_ring

Modified src/order/filter/filter_product.lean

modified def filter.bigly_equal

modified theorem filter.filter_product.lt_def'

modified theorem filter.filter_product.lt_def

modified theorem filter.filter_product.max_def

modified theorem filter.filter_product.min_def

modified theorem filter.filter_product.of_abs

modified theorem filter.filter_product.of_div

modified theorem filter.filter_product.of_eq

modified theorem filter.filter_product.of_lt

modified theorem filter.filter_product.of_lt_of_lt

modified theorem filter.filter_product.of_max

modified theorem filter.filter_product.of_min

modified theorem filter.filter_product.of_ne

modified theorem filter.filter_product.of_rel

modified theorem filter.filter_product.of_rel_of_rel

modified theorem filter.filter_product.of_rel_of_rel₂

modified theorem filter.filter_product.of_rel₂

modified theorem filter.filter_product.of_seq_add

modified theorem filter.filter_product.of_seq_fun

modified theorem filter.filter_product.of_seq_fun₂

modified theorem filter.filter_product.of_seq_mul