[Merged by Bors] - feat: Incidence algebras #8900

YaelDillies · 2023-12-08T12:54:40Z

Define incidence algebras

From LeanCamCombi

Co-authored-by: Alex J. Best alex.j.best@gmail.com

github-actions · 2024-10-04T10:03:13Z

PR summary e755ff8535

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Combinatorics.Enumerative.IncidenceAlgebra`	736

Declarations diff

+ Icc_orderDual_def
+ Ici_orderDual_def
+ Ico_orderDual_def
+ Iic_orderDual_def
+ Iio_orderDual_def
+ IncidenceAlgebra
+ Ioc_orderDual_def
+ Ioi_orderDual_def
+ Ioo_orderDual_def
+ add_apply
+ algebraRight
+ apply_eq_zero_of_not_le
+ coe_add
+ coe_constSMul
+ coe_inj
+ coe_mk
+ coe_neg
+ coe_sub
+ coe_zero
+ constSMul_apply
+ ext
+ instAdd
+ instAddCommGroup
+ instAddCommMonoid
+ instAddGroup
+ instAddMonoid
+ instFunLike
+ instInhabited
+ instIsScalarTower
+ instMul
+ instNeg
+ instNonAssocSemiring
+ instNonUnitalNonAssocSemiring
+ instOne
+ instRing
+ instSMul
+ instSemiring
+ instSmulZeroClassRight
+ instSub
+ instZero
+ instance [Preorder α] [LocallyFiniteOrder α] [DecidableEq α] [Semiring 𝕜] [Semiring 𝕝]
+ lambda
+ le_of_ne_zero
+ mk_coe
+ moduleRight
+ moebius_inversion_bot
+ moebius_inversion_top
+ mu
+ mu_apply
+ mu_eq_neg_sum_Ico_of_ne
+ mu_eq_neg_sum_Ioc_of_ne
+ mu_mul_zeta
+ mu_ofDual
+ mu_prod_mu
+ mu_self
+ mu_toDual
+ mul_apply
+ neg_apply
+ one_apply
+ one_prod_one
+ prod
+ prod_apply
+ prod_mk
+ prod_mul_prod
+ prod_mul_prod'
+ smulWithZeroRight
+ smul_apply
+ sub_apply
+ sum_Icc_mu_left
+ sum_Icc_mu_right
+ toFun_eq_coe
+ zero_apply
+ zeta
+ zeta_apply
+ zeta_mul_kappa
+ zeta_mul_mu
+ zeta_mul_zeta
+ zeta_of_le
+ zeta_prod_apply
+ zeta_prod_mk
+ zeta_prod_zeta

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.

Mathlib/Algebra/Order/Incidence.lean

YaelDillies · 2024-10-18T11:51:01Z

Mathlib/Algebra/Order/Incidence.lean

+/-! -/
+-- fake module docstring just so that I can disable the long line linter without getting linted for
+-- a missing module docstring!
+
+set_option linter.style.longLine false in
+/-!


@grunweg, you might want to investigate 😇

Good question! @damiano You are the expert on this part - with the header linter, what's the best way to silence the linter here? One should certainly be able to do (untested)

set_option linter.style header false in set_option linter.style.longLine false in stuff

To be clear, I would be even happier if #8900 (comment) didn't trigger the long line linter at all

YaelDillies · 2024-10-18T11:51:27Z

Mathlib/Algebra/Order/Incidence.lean

+
+* [Aigner, *Combinatorial Theory, Chapter IV*][aigner1997]
+* [Jacobson, *Basic Algebra I, 8.6*][jacobson1989]
+* [Doubilet, Rota, Stanley, *On the foundations of Combinatorial Theory VI*][doubilet_rota_stanley_vi]


This is the line that's too long

Define incidence algebras From LeanCamCombi Co-authored-by: Alex J. Best <alex.j.best@gmail.com>

Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean

Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>

b-mehta

bors d+

mathlib-bors · 2024-11-10T17:12:56Z

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

YaelDillies · 2024-11-11T17:41:23Z

bors merge

Define incidence algebras From LeanCamCombi Co-authored-by: Alex J. Best <alex.j.best@gmail.com>

mathlib-bors · 2024-11-11T18:30:50Z

Pull request successfully merged into master.

Build succeeded:

FR-vdash-bot · 2024-11-14T10:55:39Z

docs/references.bib

@@ -2035,6 +2067,19 @@ @Book{            Jacobson1956
  zbl           = {0073.02002}
 }

+@Book{            jacobson1989,
+  author        = {Jacobson, Nathan},
+  title         = {Basic algebra. {II}},


Shouldn't this be Basic Algebra I?

Thanks for spotting! I've opened #19027

fpvandoorn added the awaiting-author A reviewer has asked the author a question or requested changes label Apr 5, 2024

grunweg added the t-combinatorics Combinatorics label Aug 15, 2024

YaelDillies force-pushed the kneser branch from aabbe51 to 39f379c Compare October 4, 2024 10:02

YaelDillies changed the title ~~feat: Kneser's addition theorem~~ feat: Incidence algebras Oct 4, 2024

YaelDillies added t-algebra Algebra (groups, rings, fields, etc) t-order Order theory and removed awaiting-author A reviewer has asked the author a question or requested changes labels Oct 4, 2024

b-mehta reviewed Oct 17, 2024

View reviewed changes

b-mehta added the awaiting-author A reviewer has asked the author a question or requested changes label Oct 17, 2024

YaelDillies force-pushed the kneser branch from c60dc25 to 185a7b3 Compare October 17, 2024 20:10

YaelDillies removed the awaiting-author A reviewer has asked the author a question or requested changes label Oct 18, 2024

YaelDillies commented Oct 18, 2024

View reviewed changes

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 Oct 21, 2024

YaelDillies and others added 2 commits October 21, 2024 21:48

feat: Incidence algebras

3f62c32

Define incidence algebras From LeanCamCombi Co-authored-by: Alex J. Best <alex.j.best@gmail.com>

move

2d4235d

YaelDillies force-pushed the kneser branch from 37b1d9d to 2d4235d Compare October 21, 2024 21:49

YaelDillies removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-algebra Algebra (groups, rings, fields, etc) t-order Order theory labels Oct 21, 2024

fix

fce0180

YaelDillies requested a review from b-mehta November 10, 2024 09:36

b-mehta reviewed Nov 10, 2024

View reviewed changes

Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean Show resolved Hide resolved

Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean Outdated Show resolved Hide resolved

Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean Outdated Show resolved Hide resolved

Bhavik's comments

67e8a1c

Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>

b-mehta reviewed Nov 10, 2024

View reviewed changes

leanprover-community-mathlib4-bot added the delegated label Nov 10, 2024

Bhavik's whitespace

e755ff8

mathlib-bors bot pushed a commit that referenced this pull request Nov 11, 2024

feat: Incidence algebras (#8900)

fa330e6

Define incidence algebras From LeanCamCombi Co-authored-by: Alex J. Best <alex.j.best@gmail.com>

mathlib-bors bot changed the title ~~feat: Incidence algebras~~ [Merged by Bors] - feat: Incidence algebras Nov 11, 2024

mathlib-bors bot closed this Nov 11, 2024

mathlib-bors bot deleted the kneser branch November 11, 2024 18:30

FR-vdash-bot reviewed Nov 14, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: Incidence algebras #8900

[Merged by Bors] - feat: Incidence algebras #8900

YaelDillies commented Dec 8, 2023 •

edited

Loading

github-actions bot commented Oct 4, 2024 •

edited

Loading

Declarations diff

YaelDillies Oct 18, 2024

grunweg Oct 18, 2024

YaelDillies Oct 18, 2024

YaelDillies Oct 18, 2024

b-mehta left a comment

mathlib-bors bot commented Nov 10, 2024

YaelDillies commented Nov 11, 2024

mathlib-bors bot commented Nov 11, 2024

FR-vdash-bot Nov 14, 2024

YaelDillies Nov 14, 2024

[Merged by Bors] - feat: Incidence algebras #8900

[Merged by Bors] - feat: Incidence algebras #8900

Conversation

YaelDillies commented Dec 8, 2023 • edited Loading

github-actions bot commented Oct 4, 2024 • edited Loading

PR summary e755ff8535

Import changes for modified files

Declarations diff

YaelDillies Oct 18, 2024

Choose a reason for hiding this comment

grunweg Oct 18, 2024

Choose a reason for hiding this comment

YaelDillies Oct 18, 2024

Choose a reason for hiding this comment

YaelDillies Oct 18, 2024

Choose a reason for hiding this comment

b-mehta left a comment

Choose a reason for hiding this comment

mathlib-bors bot commented Nov 10, 2024

YaelDillies commented Nov 11, 2024

mathlib-bors bot commented Nov 11, 2024

FR-vdash-bot Nov 14, 2024

Choose a reason for hiding this comment

YaelDillies Nov 14, 2024

Choose a reason for hiding this comment

YaelDillies commented Dec 8, 2023 •

edited

Loading

github-actions bot commented Oct 4, 2024 •

edited

Loading