acornprover/acornlib
Acorn's standard library of mathematical facts.
59Stars
23Forks
37Claude Commits
ShellLanguage
First Claude commit: May 1, 2026Last Claude commit: 1mo agoDiscovered: May 2, 2026
Recent Claude Commits
Complete vertical composition of natural transformations
ae4d9cf1mo agoauthor_emailProve vertical-composition endpoints axiom for natural transformations
1131c991mo agoauthor_emailAdd vertical-composition scaffolding for natural transformations
6bdebe41mo agoauthor_emailAdd identity natural transformation
56ff8e01mo agoauthor_emailAdd NaturalTransformation structure between functors
df8a9781mo agoauthor_emailAdd compose_functor constructor
1aff3751mo agoauthor_emailAdd terminal category and Functor structure
4abffc61mo agoauthor_emailAdd product category construction
54b92fa1mo agoauthor_emailUpdate build artifacts
41fcc4b1mo agoauthor_emailAdd opposite category construction
756c4001mo agoauthor_emailAdd discrete category construction
08e92b21mo agoauthor_emailAdd Iso[O, M] structure for category isomorphisms
5351fd41mo agoauthor_emailAdd per-qrel kernel-quotient lifts for linear maps
66416e71mo agoauthor_emailAdd per-qrel kernel-quotient lifts for MonoidHom and AddMonoidHom
68d47f01mo agoauthor_emailAdd per-qrel kernel-quotient operation lifts for AddGroupHom, GroupHom, and RingHom
ddfe97b1mo agoauthor_emailAdd respects_mul / respects_inverse for normal subgroup relation
bc9fc321mo agoauthor_emailAdd pointwise mul/inv step lemmas for normal subgroup quotient relation
3a4c7511mo agoauthor_emailfeat: foundational normal subgroup definition and quotient relation helpers
327a8e41mo agoauthor_emailfeat: lift + and - through additive-subgroup quotient
ecfaf0a1mo agoauthor_emailfeat: subgroup quotient respects negation and addition for AddCommGroup
0a159c11mo agoauthor_emailfeat: additive-subgroup quotient relation is a congruence over AddCommGroup
7a69d851mo agoauthor_emailfeat: add foundational additive subgroup API and its quotient relation
7fba0181mo agoauthor_emailfeat: bridge linear-map kernels to additive congruence and smul preservation
3f49e1b1mo agoauthor_emailfeat: bridge ring homomorphism kernels to ring congruences
ba4588d1mo agoauthor_emailfeat: bridge MonoidHom and GroupHom kernels to multiplicative congruences
d4432801mo agoauthor_emailfeat: bridge AddGroupHom kernels to additive congruences with negation
dabbb761mo agoauthor_emailfeat: add additive monoid kernel-to-congruence bridge
3f1a8441mo agoauthor_emaildocs: record migration audit for hand-simulated quotients
f7600cf1mo agoauthor_emailfeat: add kernel relation API and quotient factorization
adb50ea1mo agoauthor_emailfeat: complete round-trip set equalities for quotient subobject transport
21d48e21mo agoauthor_emailfeat: add quotient subobject transport API
0d288be1mo agoauthor_emailfeat: add pullback/pushforward distributivity over union, intersection, converse
f99af2a1mo agoauthor_emailfeat: add compose lemmas relating single steps to refl-trans closure
faf73f91mo agoauthor_emailfeat: add step, self-composition, and converse lemmas for relation closures
367909a1mo agoauthor_emailfeat: distribute relation composition over union and intersection
046f3db1mo agoauthor_emailfeat: add equivalence closure of relations
a85be1c1mo agoauthor_emailfeat: add closure laws for transitive and reflexive-transitive closures
aa322721mo agoauthor_email