Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-08 20:32 662786a8

View on Github →

refactor(data/{finite,fintype}): redefine infinite in terms of finite, move to data.finite.defs (#16390)

Estimated changes

Modified src/data/finite/basic.lean

deleted theorem finite_or_infinite

Modified src/data/finite/defs.lean

modified theorem finite.of_bijective

added theorem finite_or_infinite

added theorem not_finite

added theorem not_finite_iff_infinite

added theorem not_infinite_iff_finite

Modified src/data/fintype/basic.lean

added theorem infinite.of_not_fintype

deleted theorem not_finite

deleted theorem not_finite_iff_infinite

deleted theorem not_infinite_iff_finite

Modified src/data/fintype/card_embedding.lean

modified theorem fintype.card_embedding_eq_of_infinite

Modified src/data/set/finite.lean

deleted theorem set.infinite.to_subtype

Modified src/field_theory/is_alg_closed/basic.lean