Commit 2025-08-17 06:12 26a03059

View on Github →

chore: remove Cardinal imports from GroupTheory.GroupAction.Quotient (#28529)

Estimated changes

Modified Mathlib/Algebra/Polynomial/GroupRingAction.lean

Modified Mathlib/Analysis/Convex/Topology.lean

Modified Mathlib/Analysis/Normed/Module/Convex.lean

Modified Mathlib/Analysis/NormedSpace/Connected.lean

Modified Mathlib/GroupTheory/GroupAction/CardCommute.lean

added theorem MulAction.card_eq_sum_card_group_div_card_stabilizer'

added theorem MulAction.card_eq_sum_card_group_div_card_stabilizer

Modified Mathlib/GroupTheory/GroupAction/Quotient.lean

deleted theorem MulAction.card_eq_sum_card_group_div_card_stabilizer'

deleted theorem MulAction.card_eq_sum_card_group_div_card_stabilizer

Modified Mathlib/LinearAlgebra/Alternating/DomCoprod.lean

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

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

Modified Mathlib/Topology/CWComplex/Classical/Basic.lean

Modified Mathlib/Topology/Germ.lean

Modified scripts/noshake.json