[Merged by Bors] - chore(Data/Finset): don't import algebra when defining `Finset.card` by Vierkantor · Pull Request #21866 · leanprover-community/mathlib4

Vierkantor · 2025-02-14T10:29:24Z

This PR aims to define Finset.card and Fintype.card without importing anything from the algebra library. In addition to the changes of #21840, we modify a few proofs and move a few lemmas so that Data.Finset.Card doesn't need to know about monoids.

depends on: [Merged by Bors] - chore(Data/Fintype): split Fintype/Card.lean #21840

github-actions · 2025-02-14T10:30:18Z

PR summary a08e4a8748

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Data.Finset.Card	412	403	-9 (-2.18%)
Mathlib.Data.Fintype.Card	424	415	-9 (-2.12%)
Mathlib.Combinatorics.SetFamily.Intersecting	453	444	-9 (-1.99%)

Import changes for all files

Files	Import difference
7 files `Mathlib.Combinatorics.SetFamily.Compression.Down` `Mathlib.Combinatorics.SetFamily.Intersecting` `Mathlib.Data.Finset.Card` `Mathlib.Data.Finset.Fin` `Mathlib.Data.Finset.Max` `Mathlib.Data.Fintype.Card` `Mathlib.Data.Fintype.Lattice`	-9
`Mathlib.Order.CountableDenseLinearOrder`	-8
`Mathlib.Algebra.Group.TypeTags.Fintype`	-6
`Mathlib.Data.Fintype.Parity`	-1
`Mathlib.Combinatorics.Additive.Corner.Roth` `Mathlib.Combinatorics.SimpleGraph.Triangle.Removal`	1
`Mathlib.Data.Finset.CastCard` (new file)	412

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

YaelDillies

This is great!

Mathlib/Data/Fintype/Card.lean

YaelDillies · 2025-02-20T10:18:35Z

Mathlib/Data/Finset/CastCard.lean

I would like such a file to be under Algebra, but I'm not sure how to call it... Is there any file it could merge with?

I can't easily find a mergeable file right now (see error messages below in case you want to debug ImportGraph). I would even consider placing it under Data.Int.Cast.

$ lake exe graph --from Mathlib.Data.Finset.Card Mathlib.Data.Int.Cast.Basic cast-card-options.pdf && open cast-card-options.pdf Error occurred while writing out Mathlib.Data.Int.Cast.Basic. Make sure you have `graphviz` installed and the file is writable. uncaught exception: resource vanished (error code: 32, broken pipe)

(lake exe graph worked fine a couple minutes ago...)

Mathlib/Data/Finset/Card.lean

Co-authored-by: Yaël Dillies <[email protected]>

mathlib4-dependent-issues-bot · 2025-02-20T10:35:42Z

This PR/issue depends on:

~~[Merged by Bors] - chore(Data/Fintype): split Fintype/Card.lean #21840~~
By Dependent Issues (🤖). Happy coding!

YaelDillies

We can rename Data.Finset.CastCard later

maintainer merge

github-actions · 2025-02-20T12:46:28Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

riccardobrasca · 2025-02-20T12:54:58Z

Thanks!

bors merge

…21866) This PR aims to define `Finset.card` and `Fintype.card` without importing anything from the algebra library. In addition to the changes of #21840, we modify a few proofs and move a few lemmas so that `Data.Finset.Card` doesn't need to know about monoids. Co-authored-by: Anne Baanen <[email protected]>

mathlib-bors · 2025-02-20T13:57:01Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: (823 commits) chore(Computability): fix naming of lemmas about Sum.inl, Sum.inr, Sum.casesOn (#22156) feat: `Fintype Ordering` (#22154) chore: more renamings to fit the naming convention (#22148) feat(CategoryTheory): any monomorphism in a Grothendieck abelian category is a transfinite composition of pushouts of monomorphisms in a small family (#22157) chore: rename `{Continuous., continuous_}sum_map` to `sumMap` (#22155) chore: remove initial space followed by `-/` (#22158) chore: make arg in HeightOneSpectrum.valuation explicit (#22139) feat(Data/List): `List.maximum` is monotone (#22091) chore(Combinatorics/SimpleGraph): extract WalkDecomp from Walk (#21981) feat: if a monoid M acts, then so does (s : S) with [SubmonoidClass S M] (#21123) chore: backport changes to `getElem` lemmas (#22146) feat(CategoryTheory): generating monomorphisms in Grothendieck abelian categories (#22150) feat: rename variables to fit doc (#22143) feat(CategoryTheory): IsDetecting.isIso_iff_of_mono (#22135) feat(CategoryTheory): truncations of transfinite compositions (#22149) chore: simplify a proof (#22134) feat(CategoryTheory): monomorphisms are stable under coproducts in Grothendieck abelian categories (#22133) feat(Order): Set.Ici.isSuccLimit_coe (#22103) chore(Analysis/Convex/Normed): split into smaller files (#22015) feat(Algebra/Algebra/Lie): max nilpotent ideal <= radical (#22140) refactor(LinearIndependent): refactor to use LinearIndepOn (#21886) chore: rename some more `Foo.sum_elim` -> `sumElim` (#22130) chore: rename Injective.sum_elim and friends (#22129) chore: fix naming oversight from #22070 (#22128) chore: fix spelling mistakes (#22136) feat(RingTheory/Ideal/Quotient): define transtition map between ring or module quotient by powers of ideal (#21900) fix: initialize_simps_projections print warning when projection data already exists (#20339) chore: rename ContMDiff.sum_{elim,map} (#22131) feat(CategoryTheory): characterization of injective objects in terms of lifting properties (#22104) chore(Lean,Tactic): un-indent some doc-strings (#22118) feat(Algebra/MvPolynomial): add `comp` versions of rename lemmas (#21259) chose: add deprecation (#22124) feat(CategoryTheory/Abelian/GrothendieckCategory): computing colimits in Subobject (#22123) feat(CategoryTheory/Subobject): hasCardinalLT_of_mono (#22122) feat: add `DenseRange.piMap` (#22114) feat(Algebra/Algebra/Lie): define the maximal nilpotent ideal of Lie algebras (#22061) chore(Data/Finset): don't import algebra when defining `Finset.card` (#21866) feat: a function on a discrete space is smooth (#22113) feat: commutative group objects in additive categories (#21521) style(Geometry/Manifold): remove superfluous indentation in doc-strings (#22117) chore: rename PushNeg.lean to Push.lean (#22108) feat: add Is{Open,Closed}Embedding.sum_elim (#22070) feat(RingTheory/Perfectoid): define the untilt map and generalize pretilt (#21563) feature(Topology/Algebra/Module/WeakBilin): Linear map from F into the topological dual of E with the weak topology (#21078) feat(CategoryTheory/Abelian): the exact sequence attached to a pushout square (#22110) chore(ChartedSpace.lean): group constructions together (#22107) feat(CategoryTheory/MorphismProperty): more basic API (#22099) chore(Data/Fintype): split `Fintype/Card.lean` (#21840) chore(SetTheory/Cardinal/Cofinality): make `IsStrongLimit` into a structure (#21971) feat(Combinatorics/SimpleGraph): Add a theorem about cliques in induced subgraphs (#20705) ...

@pechersky

* polynomial-sequences: (558 commits) Correct the TODO to mention IsCancelAdd which does exist. Talk about strict monotonicity instead, thanks @pechersky. Mention the TODO on li generalization to semirings. One more dedent. Same injectivity twiddling for basis. nontiviality to simplify this proof, and some dedenting. Hopefully more correct injectivity lemmas matching the naming convention. Fix the empty docstring. Update Mathlib/Algebra/Polynomial/Sequence.lean Fix the variable naming. Apply suggestions from code review chore(Computability): fix naming of lemmas about Sum.inl, Sum.inr, Sum.casesOn (#22156) feat: `Fintype Ordering` (#22154) chore: more renamings to fit the naming convention (#22148) feat(CategoryTheory): any monomorphism in a Grothendieck abelian category is a transfinite composition of pushouts of monomorphisms in a small family (#22157) chore: rename `{Continuous., continuous_}sum_map` to `sumMap` (#22155) chore: remove initial space followed by `-/` (#22158) chore: make arg in HeightOneSpectrum.valuation explicit (#22139) feat(Data/List): `List.maximum` is monotone (#22091) chore(Combinatorics/SimpleGraph): extract WalkDecomp from Walk (#21981) feat: if a monoid M acts, then so does (s : S) with [SubmonoidClass S M] (#21123) chore: backport changes to `getElem` lemmas (#22146) feat(CategoryTheory): generating monomorphisms in Grothendieck abelian categories (#22150) feat: rename variables to fit doc (#22143) feat(CategoryTheory): IsDetecting.isIso_iff_of_mono (#22135) feat(CategoryTheory): truncations of transfinite compositions (#22149) chore: simplify a proof (#22134) feat(CategoryTheory): monomorphisms are stable under coproducts in Grothendieck abelian categories (#22133) feat(Order): Set.Ici.isSuccLimit_coe (#22103) chore(Analysis/Convex/Normed): split into smaller files (#22015) feat(Algebra/Algebra/Lie): max nilpotent ideal <= radical (#22140) refactor(LinearIndependent): refactor to use LinearIndepOn (#21886) chore: rename some more `Foo.sum_elim` -> `sumElim` (#22130) chore: rename Injective.sum_elim and friends (#22129) chore: fix naming oversight from #22070 (#22128) chore: fix spelling mistakes (#22136) feat(RingTheory/Ideal/Quotient): define transtition map between ring or module quotient by powers of ideal (#21900) fix: initialize_simps_projections print warning when projection data already exists (#20339) chore: rename ContMDiff.sum_{elim,map} (#22131) feat(CategoryTheory): characterization of injective objects in terms of lifting properties (#22104) chore(Lean,Tactic): un-indent some doc-strings (#22118) feat(Algebra/MvPolynomial): add `comp` versions of rename lemmas (#21259) chose: add deprecation (#22124) feat(CategoryTheory/Abelian/GrothendieckCategory): computing colimits in Subobject (#22123) feat(CategoryTheory/Subobject): hasCardinalLT_of_mono (#22122) feat: add `DenseRange.piMap` (#22114) feat(Algebra/Algebra/Lie): define the maximal nilpotent ideal of Lie algebras (#22061) chore(Data/Finset): don't import algebra when defining `Finset.card` (#21866) feat: a function on a discrete space is smooth (#22113) feat: commutative group objects in additive categories (#21521) ...

Vierkantor added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-data Data (lists, quotients, numbers, etc) labels Feb 14, 2025

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 14, 2025

Vierkantor force-pushed the no-Monoid-in-Finset.Card branch from 8046841 to f17288b Compare February 14, 2025 11:06

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Feb 14, 2025

Vierkantor mentioned this pull request Feb 14, 2025

[Merged by Bors] - chore(Data/Set/Finite): avoid importing algebra in Data.Set.Finite #21870

Closed

1 task

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 14, 2025

Vierkantor added 6 commits February 20, 2025 11:09

chore(Data/Finset): don't import algebra when defining Finset.card

edffb08

Fixes downstream

6008478

Shake

4ef3763

More shaking

a4124d5

Readd missing import

e77324f

Back to shaking again!

13c4659

Vierkantor force-pushed the no-Monoid-in-Finset.Card branch from df9d836 to 13c4659 Compare February 20, 2025 10:10

Vierkantor removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 20, 2025

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 20, 2025

YaelDillies reviewed Feb 20, 2025

View reviewed changes

Vierkantor commented Feb 20, 2025

View reviewed changes

Mathlib/Data/Finset/Card.lean Outdated Show resolved Hide resolved

Deredundantify assert_not_exists

a08e4a8

Co-authored-by: Yaël Dillies <[email protected]>

YaelDillies approved these changes Feb 20, 2025

View reviewed changes

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Feb 20, 2025

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Feb 20, 2025

mathlib-bors bot changed the title ~~chore(Data/Finset): don't import algebra when defining Finset.card~~ [Merged by Bors] - chore(Data/Finset): don't import algebra when defining Finset.card Feb 20, 2025

mathlib-bors bot closed this Feb 20, 2025

mathlib-bors bot deleted the no-Monoid-in-Finset.Card branch February 20, 2025 13:57

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore(Data/Finset): don't import algebra when defining `Finset.card`#21866

[Merged by Bors] - chore(Data/Finset): don't import algebra when defining `Finset.card`#21866
Vierkantor wants to merge 7 commits intomasterfrom
no-Monoid-in-Finset.Card

Vierkantor commented Feb 14, 2025 •

edited by YaelDillies

Loading

Uh oh!

github-actions bot commented Feb 14, 2025 •

edited

Loading

Import changes for modified files

Uh oh!

YaelDillies left a comment

Uh oh!

Uh oh!

YaelDillies Feb 20, 2025

Uh oh!

Vierkantor Feb 20, 2025

Uh oh!

Uh oh!

mathlib4-dependent-issues-bot commented Feb 20, 2025

Uh oh!

YaelDillies left a comment

Uh oh!

github-actions bot commented Feb 20, 2025

Uh oh!

riccardobrasca commented Feb 20, 2025

Uh oh!

mathlib-bors bot commented Feb 20, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Conversation

Vierkantor commented Feb 14, 2025 • edited by YaelDillies Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Feb 14, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary a08e4a8748

Import changes for modified files

Declarations diff

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

YaelDillies Feb 20, 2025

Choose a reason for hiding this comment

Uh oh!

Vierkantor Feb 20, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

mathlib4-dependent-issues-bot commented Feb 20, 2025

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Feb 20, 2025

Uh oh!

riccardobrasca commented Feb 20, 2025

Uh oh!

mathlib-bors bot commented Feb 20, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Vierkantor commented Feb 14, 2025 •

edited by YaelDillies

Loading

github-actions bot commented Feb 14, 2025 •

edited

Loading