Commit 2024-08-16 23:11 61b9d5e7

View on Github →

chore: avoid importing Cardinal in basic group theory (#15646)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/Grp/Colimits.lean

Modified Mathlib/Algebra/Category/Grp/EpiMono.lean

Modified Mathlib/Algebra/CharZero/Quotient.lean

Modified Mathlib/Algebra/ModEq.lean

Modified Mathlib/Algebra/Order/ToIntervalMod.lean

Modified Mathlib/Algebra/Periodic.lean

Modified Mathlib/Algebra/Pointwise/Stabilizer.lean

Modified Mathlib/Data/ZMod/Basic.lean

Modified Mathlib/GroupTheory/Abelianization.lean

Renamed Mathlib/GroupTheory/Commutator.lean to Mathlib/GroupTheory/Commutator/Basic.lean

deleted theorem Subgroup.commutator_pi_pi_of_finite

Created Mathlib/GroupTheory/Commutator/Finite.lean

added theorem Subgroup.commutator_pi_pi_of_finite

Modified Mathlib/GroupTheory/CommutingProbability.lean

Renamed Mathlib/GroupTheory/Coset.lean to Mathlib/GroupTheory/Coset/Basic.lean

deleted theorem Subgroup.card_comap_dvd_of_injective

deleted theorem Subgroup.card_dvd_of_injective

deleted theorem Subgroup.card_dvd_of_le

deleted theorem Subgroup.card_eq_card_quotient_mul_card_subgroup

deleted theorem Subgroup.card_quotient_dvd_card

deleted theorem Subgroup.card_subgroup_dvd_card

Created Mathlib/GroupTheory/Coset/Card.lean

added theorem Subgroup.card_comap_dvd_of_injective

added theorem Subgroup.card_dvd_of_injective

added theorem Subgroup.card_dvd_of_le

added theorem Subgroup.card_eq_card_quotient_mul_card_subgroup

added theorem Subgroup.card_quotient_dvd_card

added theorem Subgroup.card_subgroup_dvd_card

Modified Mathlib/GroupTheory/Coxeter/Basic.lean

Modified Mathlib/GroupTheory/Divisible.lean

Modified Mathlib/GroupTheory/DoubleCoset.lean

Modified Mathlib/GroupTheory/Finiteness.lean

Created Mathlib/GroupTheory/GroupAction/CardCommute.lean

added theorem card_comm_eq_card_conjClasses_mul_card

Modified Mathlib/GroupTheory/GroupAction/Quotient.lean

deleted theorem card_comm_eq_card_conjClasses_mul_card

Modified Mathlib/GroupTheory/Index.lean

Modified Mathlib/GroupTheory/Nilpotent.lean

Modified Mathlib/GroupTheory/OrderOfElement.lean

Modified Mathlib/GroupTheory/PresentedGroup.lean

Renamed Mathlib/GroupTheory/QuotientGroup.lean to Mathlib/GroupTheory/QuotientGroup/Basic.lean

Created Mathlib/GroupTheory/QuotientGroup/Finite.lean

Modified Mathlib/GroupTheory/SpecificGroups/Alternating.lean

Modified Mathlib/GroupTheory/SpecificGroups/Dihedral.lean

Modified Mathlib/LinearAlgebra/Alternating/DomCoprod.lean

Modified Mathlib/LinearAlgebra/Quotient.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

Modified Mathlib/RingTheory/ClassGroup.lean

Modified Mathlib/Topology/Algebra/Group/Basic.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Group.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Nonarchimedean.lean

Modified Mathlib/Topology/Algebra/Ring/Basic.lean