feat: the club filter

[vihdzp]

---

• depends on: [Merged by Bors] - feat: stationary sets #39727

[github-actions]

PR summary 7151ebdefc

Import changes exceeding 2%

%	File
+16.98%	Mathlib.Algebra.Ring.BooleanRing

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Ring.BooleanRing	536	627	+91 (+16.98%)

Import changes for all files

Files	Import difference
Mathlib.Algebra.Category.BoolRing	64
Mathlib.Algebra.Ring.BooleanRing	91
Mathlib.SetTheory.Cardinal.Cofinality.Filter (new file)	908

---

Declarations diff

+ AsBoolAlg.rec
+ AsBoolRing.rec
+ IsClub.isStationary
+ IsCofinal.nonempty
+ IsStationary
+ IsStationary.mono
+ IsStationary.nonempty
+ IsStationary.of_not_isCofinal_compl
+ IsStationary.univ
+ Order.IsNormal.isClub_range
+ StationarySet
+ _root_.isClub_empty_iff
+ cardinalInterFilter_clubFilter
+ clubFilter
+ countableInterFilter_clubFilter
+ iInter_of_countable
+ instance (I : Ideal α) [I.IsTwoSided] : BooleanRing (α ⧸ I)
+ instance : BooleanAlgebra (StationarySet α)
+ isStationary_iUnion_iff
+ isStationary_iUnion_iff_of_cof_le_one
+ isStationary_iUnion_iff_of_countable
+ isStationary_iUnion_iff_of_orderTop
+ isStationary_sUnion_iff
+ isStationary_sUnion_iff_of_cof_le_one
+ isStationary_sUnion_iff_of_countable
+ isStationary_sUnion_iff_of_orderTop
+ isStationary_union_iff
+ isStationary_univ_iff
+ mem_clubFilter
+ mem_nonstationaryIdeal_iff
+ mk
+ mk_compl
+ mk_empty
+ mk_eq_bot
+ mk_eq_mk
+ mk_inter
+ mk_of_not_isStationary
+ mk_sdiff
+ mk_symmDiff
+ mk_union
+ mk_univ
+ nonempty
+ nonstationaryIdeal
+ not_isStationary_empty
+ not_isStationary_iff
+ not_isStationary_of_isEmpty
+ sInter_of_countable
+ toBoolRing_compl
+ toBoolRing_sdiff
+ toBoolRing_sup
- _root_.Order.IsNormal.isClub_range

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[mathlib-bors]

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - feat: stationary sets #39727
  By Dependent Issues (🤖). Happy coding!

[j-loreaux]

@vihdzp if you merge master and finish prepping this PR, I'll review it if you ping me.

[vihdzp]

This PR inadvertently turned into 2, I'll split the stuff on the club filter into a new PR.