Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-24 16:04 b4373e5a

View on Github →

feat(tactic/lint): linter for @[class] def (#6061) Also cleaning up some uses of @[class] def that were missed in #6028.

Estimated changes

modified theorem add_pow_char_of_commute
modified theorem fact.succ.pos
modified def fin.of_nat'
modified theorem padic_val_nat_primes
added theorem set.ord_connected.out
deleted def set.ord_connected
added theorem set.ord_connected_def
modified theorem set.ord_connected_empty
modified theorem set.ord_connected_univ
modified theorem zmod.frobenius_zmod
modified theorem fact_zero_lt_one
modified theorem fact.elim
deleted def fact
added theorem fact_iff
modified theorem fact_one_le_one_ennreal
modified theorem fact_one_le_top_ennreal
modified theorem zmod.eisenstein_lemma
added theorem zmod.fact_prime_two
modified theorem zmod.gauss_lemma
modified theorem algebra.finite_type.self
deleted def algebra.finite_type
modified theorem module.finite.trans
deleted def module.finite
modified theorem module.finite_def
deleted def module.flat
modified def nonote.of_nat
deleted def onote.NF
deleted inductive pSet.definable
modified theorem T.zero_lt_one
modified theorem abs_nonneg'
modified def primality_test