Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-30 20:43 6e0d0fa4

View on Github →

chore(algebra/field): use K as a type variable (#5535)

Estimated changes

Modified src/algebra/field.lean

modified theorem add_div'

modified theorem add_div

modified theorem add_div_eq_mul_add_div

modified theorem div_add'

modified theorem div_add_div

modified theorem div_add_div_same

modified theorem div_neg

modified theorem div_neg_eq_neg_div

modified theorem div_sub'

modified theorem div_sub_div

modified theorem div_sub_div_same

modified theorem inv_add_inv

modified theorem inv_sub_inv

modified theorem inverse_eq_has_inv

modified theorem mul_div_assoc'

modified theorem neg_div'

modified theorem neg_div

modified theorem neg_div_neg_eq

modified theorem one_div_add_one_div

modified theorem one_div_neg_eq_neg_one_div

modified theorem one_div_neg_one_eq_neg_one

modified theorem sub_div'

modified theorem sub_div