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

  • fintype → finite 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 is_p_group.is_nilpotent
modified theorem nilpotency_class_pi
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
modified theorem equiv.perm.is_cycle.pow_iff
modified theorem equiv.perm.same_cycle.nat''
modified theorem equiv.perm.same_cycle.nat'
modified theorem equiv.perm.closure_is_swap
modified theorem monoid_hom.eq_on_closure
modified theorem subgroup.bot_or_nontrivial
modified theorem subgroup.pi_le_iff
modified theorem not_dvd_index_sylow
modified theorem sylow.normalizer_normalizer
modified theorem sylow.orbit_eq_top
added theorem is_torsion_of_finite
deleted theorem is_torsion_of_fintype