Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-24 06:28 4b9cdf44

View on Github →

chore(*): pass dup_namespace and def_lemma lint tests (#1599)

  • chore(*): pass dup_namespace and def_lemma lint tests
  • Update src/group_theory/free_group.lean Co-Authored-By: Johan Commelin johan@commelin.net
  • Update src/number_theory/pell.lean Co-Authored-By: Johan Commelin johan@commelin.net
  • Update src/order/lattice.lean Co-Authored-By: Johan Commelin johan@commelin.net
  • Update src/set_theory/ordinal.lean Co-Authored-By: Johan Commelin johan@commelin.net
  • Update src/set_theory/ordinal.lean Co-Authored-By: Johan Commelin johan@commelin.net
  • Update src/tactic/transfer.lean Co-Authored-By: Johan Commelin johan@commelin.net
  • Update src/group_theory/free_group.lean Co-Authored-By: Reid Barton rwbarton@gmail.com
  • using nolint

Estimated changes

modified theorem free_group.sum.sum
modified def pell.pell
added theorem lattice.ext
deleted theorem lattice.lattice.ext
modified theorem zorn.zorn
modified def cardinal.ord_eq_min
modified def ordinal.div_def