Commit 2025-08-12 12:14 11fa48cf

View on Github →

chore: postpone some Cardinal imports (#28277) See #mathlib4 > Warning that AlgebraicTopology can't import SetTheory @ 💬. This postpones the theory of cardinals further through the basics of linear algebra.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Exact.lean

Modified Mathlib/Algebra/FiveLemma.lean

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

Modified Mathlib/Algebra/Module/Presentation/Free.lean

Modified Mathlib/Analysis/Convex/Combination.lean

Modified Mathlib/LinearAlgebra/Isomorphisms.lean

Modified Mathlib/LinearAlgebra/Quotient/Basic.lean

deleted theorem Submodule.card_eq_card_quotient_mul_card

Created Mathlib/LinearAlgebra/Quotient/Card.lean

added theorem Submodule.card_eq_card_quotient_mul_card

Modified Mathlib/LinearAlgebra/TensorProduct/Quotient.lean

Modified Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean

Modified Mathlib/RingTheory/Jacobson/Radical.lean

Modified Mathlib/RingTheory/Nilpotent/Lemmas.lean