Commit 2024-08-08 15:42 54ff6aaa

View on Github →

chore: avoid import Cardinal unnecessarily (#15580)

Estimated changes

Modified Counterexamples/MapFloor.lean

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Operations.lean

Modified Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

Modified Mathlib/Algebra/Algebra/Subalgebra/Operations.lean

Modified Mathlib/Algebra/Group/UniqueProds.lean

Modified Mathlib/Algebra/MonoidAlgebra/Support.lean

Modified Mathlib/Algebra/Order/Antidiag/Pi.lean

Modified Mathlib/Algebra/Pointwise/Stabilizer.lean

Modified Mathlib/Algebra/Polynomial/Degree/Definitions.lean

Modified Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean

Modified Mathlib/Algebra/Vertex/HVertexOperator.lean

Modified Mathlib/Combinatorics/Additive/ETransform.lean

Modified Mathlib/Combinatorics/Additive/Energy.lean

Modified Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean

Modified Mathlib/Combinatorics/Additive/RuzsaCovering.lean

Modified Mathlib/Data/Complex/Module.lean

Modified Mathlib/Data/DFinsupp/Interval.lean

Modified Mathlib/Data/Finset/Finsupp.lean

Modified Mathlib/Data/Finset/NatDivisors.lean

Renamed Mathlib/Data/Finset/Pointwise.lean to Mathlib/Data/Finset/Pointwise/Basic.lean

deleted theorem Set.card_div_le

deleted theorem Set.card_inv

deleted theorem Set.card_mul_le

deleted theorem Set.card_smul_set

Created Mathlib/Data/Finset/Pointwise/Card.lean

added theorem Set.card_div_le

added theorem Set.card_inv

added theorem Set.card_mul_le

added theorem Set.card_smul_set

Modified Mathlib/Data/Finset/Pointwise/Interval.lean

Modified Mathlib/Data/Multiset/Interval.lean

Modified Mathlib/RingTheory/HahnSeries/Multiplication.lean

Modified scripts/style-exceptions.txt