Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

feat(algebra/incidence): Incidence algebras #11656

Closed
wants to merge 44 commits into from
Closed
Changes from all commits
Commits
Show all changes
44 commits
Select commit Hold shift + click to select a range
77d71d1
initial commit
YaelDillies Jan 1, 2022
8ef81cb
fun_like instance, additive structure, Euler characteristic
YaelDillies Jan 1, 2022
07f02dc
prove basic properties of mu
alexjbest Jan 1, 2022
577cf7c
couple proof wips
alexjbest Jan 1, 2022
0bae023
lift more instances
YaelDillies Jan 1, 2022
4df74bd
Merge branch 'incidence_algebra' of https://github.com/leanprover-com…
YaelDillies Jan 1, 2022
4d1d1eb
random
alexjbest Jan 1, 2022
cb023c5
Merge branch 'incidence_algebra' of github.com:leanprover-community/m…
alexjbest Jan 1, 2022
2fc6649
prove some things
alexjbest Jan 2, 2022
bc9b31e
proofs
alexjbest Jan 2, 2022
0064911
prove mobius inversion
alexjbest Jan 2, 2022
148e305
state bot and top versions
alexjbest Jan 2, 2022
9eaf8ca
progress on prod
alexjbest Jan 2, 2022
224a807
finish proof of moebius function on product orders
alexjbest Jan 2, 2022
6017f3c
fix some basic lemmas
alexjbest Jan 3, 2022
9c88f1e
move up finset lemmas
YaelDillies Jan 3, 2022
c2189fb
Merge branch 'incidence_algebra' of https://github.com/leanprover-com…
YaelDillies Jan 3, 2022
93197e7
proof
alexjbest Jan 3, 2022
167608b
fix
alexjbest Jan 3, 2022
62044f1
scalar instances
YaelDillies Jan 3, 2022
1b03fd0
Merge branch 'incidence_algebra' of https://github.com/leanprover-com…
YaelDillies Jan 3, 2022
b10f0ef
prove dual
alexjbest Jan 3, 2022
64409fc
classicalize
alexjbest Jan 3, 2022
82220b1
minigolf
alexjbest Jan 3, 2022
d6375e0
finish proof and add some todos
alexjbest Jan 5, 2022
feedec7
quiet
alexjbest Jan 5, 2022
f83f500
Style
alexjbest Jan 5, 2022
759b2fd
some linting
alexjbest Jan 5, 2022
eeedf20
finish preorder instance
alexjbest Jan 8, 2022
b2f78aa
sorry free
alexjbest Jan 8, 2022
0e95ffd
cleanup
alexjbest Jan 8, 2022
dcfcbed
lint clean
alexjbest Jan 8, 2022
d819a61
docs and lambda
alexjbest Jan 8, 2022
af4f6ee
Merge remote-tracking branch 'origin/master' into incidence_algebra
YaelDillies Jan 11, 2022
f8c9969
algebra instance
YaelDillies Jan 11, 2022
517d463
Merge branch 'master' of https://github.com/leanprover-community/math…
alexjbest May 9, 2023
93bfff8
bomp
alexjbest May 9, 2023
7901efe
cleanup
YaelDillies May 9, 2023
16498ed
Update src/algebra/incidence.lean
alexjbest May 9, 2023
d89f04c
Update src/algebra/incidence.lean
alexjbest May 9, 2023
064937c
golf mu_prod_mu
YaelDillies May 9, 2023
8925def
ty linter
alexjbest May 10, 2023
ba85377
style
alexjbest May 10, 2023
d166a0f
Merge tag 'port-complete' into incidence_algebra
eric-wieser Oct 11, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Loading
Loading