Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-31 16:48 49be50fb

View on Github →

doc(data/padics, data/real/cau_seq, algebra): add doc strings, remove unnecessary assumptions (#1283)

  • doc(data/padics): add doc strings, remove unnecessary prime assumptions
  • fix(data/real/cau_seq): remove unnecessary hypotheses
  • fix(algebra/{field, ordered_field}): remove unused assumptions
  • doc(data/real/cau_seq): document Cauchy sequences
  • fix(algebra/field): remove obsolete lemma
  • fix build
  • fix build
  • more unnecessary arguments
  • Update src/data/padics/padic_numbers.lean
  • Update src/data/padics/padic_numbers.lean
  • remove another unnecessary argument (suggested by @sgouezel)

Estimated changes

modified theorem div_mul_div_cancel
deleted theorem field.div_mul_div_cancel
modified theorem units.units.mk0_inj
modified theorem nat.inv_pos_of_nat
modified theorem nat.one_div_pos_of_nat
modified theorem padic.coe_inj