Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-05 12:11 34e366c6

View on Github →

refactor(*): remove uses of @[class] def (#6028) Preparation for lean 4, which does not support this idiom.

Estimated changes

deleted def irreducible
added theorem irreducible_iff
modified theorem list.left_unique_forall₂
modified theorem list.right_unique_forall₂
added theorem option.mem.left_unique
modified theorem roption.mem_unique
modified theorem computation.mem_unique
deleted def wseq.is_finite
deleted def wseq.productive
added theorem wseq.productive_iff
deleted def is_alg_closure
added theorem is_alg_closure_iff
modified theorem is_galois.integral
deleted theorem is_galois.normal
modified theorem is_galois.separable
added theorem is_galois.splits
deleted def is_galois
added theorem is_galois_iff
modified theorem normal.is_integral
added theorem normal.out
modified theorem normal.splits
deleted def normal
added theorem normal_iff
added theorem is_separable.separable
deleted def is_separable
added theorem is_separable_iff
added theorem is_Hausdorff.haus
deleted def is_Hausdorff
added theorem is_Hausdorff_iff
deleted def is_adic_complete
added theorem is_precomplete.prec
deleted def is_precomplete
added theorem is_precomplete_iff
deleted def relator.bi_total
deleted def relator.bi_unique
deleted def relator.left_total
deleted def relator.left_unique
modified theorem relator.left_unique_flip
modified theorem relator.rel_exists_of_total
modified theorem relator.rel_forall_of_total
deleted def relator.right_total
modified theorem filter.eventually_const
modified theorem filter.ne_bot.ne
deleted def filter.ne_bot
added theorem filter.ne_bot_iff
deleted def ideal.is_maximal
added theorem ideal.is_maximal_def
added theorem ideal.is_prime.ne_top
deleted def ideal.is_prime
added theorem ideal.is_prime_iff
added theorem ideal.is_jacobson.out
deleted def ideal.is_jacobson
added theorem ideal.is_jacobson_iff
deleted def ideal.is_local
added theorem ideal.is_local_iff
deleted def is_noetherian_ring
added theorem is_noetherian_ring_iff
deleted def witt_vector.is_poly
deleted def pgame.impartial
modified theorem pgame.impartial_def
deleted def separated_space
added theorem separated_space_iff