Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-17 14:53 b78cf506

View on Github →

chore(group_theory/*): Fix lint (#16095) Fix the linting errors coming from fintype_finite and to_additive_doc in the group_theory folder (+ some in data and combinatorics). Remove the decidability assumptions to decidable_powers/decidable_zpowers because they are already noncomputable.

Lemma renames

  • fintypefinite in lemmas that used to assume fintype and now only assume finite
  • fintype.induction_empty_option'fintype.induction_empty_option

Estimated changes

deleted theorem finite.exists_max
deleted theorem finite.exists_min
deleted theorem finite.of_not_infinite
deleted theorem infinite.of_not_finite
deleted theorem not_finite
deleted theorem not_finite_iff_infinite
deleted theorem not_infinite_iff_finite
added theorem finite.exists_max
added theorem finite.exists_min
deleted theorem fintype.exists_max
deleted theorem fintype.exists_min
deleted theorem fintype.exists_univ_list
added theorem not_finite
deleted theorem not_fintype
modified theorem exists_pow_eq_one
modified theorem exists_zpow_eq_one
modified theorem fin_equiv_powers_apply
modified theorem fin_equiv_powers_symm_apply
modified theorem fin_equiv_zpowers_apply
modified theorem mem_powers_iff_mem_zpowers
modified theorem order_eq_card_powers
modified theorem order_eq_card_zpowers
modified theorem order_of_le_card_univ
modified theorem order_of_pos
modified theorem order_of_pow
modified theorem pow_card_eq_one
modified theorem powers_eq_zpowers
modified theorem powers_equiv_powers_apply
modified theorem zpowers_equiv_zpowers_apply