Commit 2023-06-08 18:26 5238ba14

View on Github →

chore: tidy various files (#4854)

Estimated changes

Modified Mathlib/Algebra/AlgebraicCard.lean

added theorem Algebraic.cardinal_mk_of_countable_of_charZero

deleted theorem Algebraic.cardinal_mk_of_countble_of_charZero

Modified Mathlib/Algebra/Category/ModuleCat/Limits.lean

Modified Mathlib/Analysis/Calculus/Deriv/Basic.lean

Modified Mathlib/Analysis/Complex/UnitDisc/Basic.lean

Modified Mathlib/Analysis/NormedSpace/BallAction.lean

Modified Mathlib/CategoryTheory/Bicategory/Coherence.lean

Modified Mathlib/CategoryTheory/Limits/Fubini.lean

Modified Mathlib/FieldTheory/Minpoly/Field.lean

added theorem minpoly.dvd_map_of_isScalarTower'

deleted theorem minpoly.dvd_map_of_is_scalar_tower'

added def minpoly.rootsOfMinPolyPiType

Modified Mathlib/GroupTheory/Complement.lean

deleted theorem Subgroup.IsComplement'_bot_left

deleted theorem Subgroup.IsComplement'_bot_right

deleted theorem Subgroup.IsComplement'_bot_top

deleted theorem Subgroup.IsComplement'_comm

deleted theorem Subgroup.IsComplement'_def

deleted theorem Subgroup.IsComplement'_iff_card_mul_and_disjoint

deleted theorem Subgroup.IsComplement'_of_card_mul_and_disjoint

deleted theorem Subgroup.IsComplement'_of_coprime

deleted theorem Subgroup.IsComplement'_of_disjoint_and_mul_eq_univ

deleted theorem Subgroup.IsComplement'_stabilizer

deleted theorem Subgroup.IsComplement'_top_bot

deleted theorem Subgroup.IsComplement'_top_left

deleted theorem Subgroup.IsComplement'_top_right

deleted theorem Subgroup.IsComplement_iff_existsUnique

deleted theorem Subgroup.IsComplement_singleton_left

deleted theorem Subgroup.IsComplement_singleton_right

deleted theorem Subgroup.IsComplement_singleton_top

deleted theorem Subgroup.IsComplement_top_left

deleted theorem Subgroup.IsComplement_top_right

deleted theorem Subgroup.IsComplement_top_singleton

added theorem Subgroup.isComplement'_bot_left

added theorem Subgroup.isComplement'_bot_right

added theorem Subgroup.isComplement'_bot_top

added theorem Subgroup.isComplement'_comm

added theorem Subgroup.isComplement'_def

added theorem Subgroup.isComplement'_iff_card_mul_and_disjoint

added theorem Subgroup.isComplement'_of_card_mul_and_disjoint

added theorem Subgroup.isComplement'_of_coprime

added theorem Subgroup.isComplement'_of_disjoint_and_mul_eq_univ

added theorem Subgroup.isComplement'_stabilizer

added theorem Subgroup.isComplement'_top_bot

added theorem Subgroup.isComplement'_top_left

added theorem Subgroup.isComplement'_top_right

added theorem Subgroup.isComplement_iff_existsUnique

added theorem Subgroup.isComplement_singleton_left

added theorem Subgroup.isComplement_singleton_right

added theorem Subgroup.isComplement_singleton_top

added theorem Subgroup.isComplement_top_left

added theorem Subgroup.isComplement_top_right

added theorem Subgroup.isComplement_top_singleton

added theorem Subgroup.quotientEquivSigmaZMod_apply

added theorem Subgroup.quotientEquivSigmaZMod_symm_apply

deleted theorem Subgroup.quotientEquivSigmaZmod_apply

deleted theorem Subgroup.quotientEquivSigmaZmod_symm_apply

Modified Mathlib/GroupTheory/Perm/Cycle/Concrete.lean

Modified Mathlib/GroupTheory/SchurZassenhaus.lean

Modified Mathlib/GroupTheory/Transfer.lean

Modified Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean