acornprover/acornlib
Acorn's standard library of mathematical facts.
59Stars
24Forks
37Claude Commits
ShellLanguage
First Claude commit: May 1, 2026Last Claude commit: 2mo agoDiscovered: May 2, 2026
Recent Claude Commits
Complete vertical composition of natural transformations
ae4d9cf2mo agoauthor_emailProve vertical-composition endpoints axiom for natural transformations
1131c992mo agoauthor_emailAdd vertical-composition scaffolding for natural transformations
6bdebe42mo agoauthor_emailAdd identity natural transformation
56ff8e02mo agoauthor_emailAdd NaturalTransformation structure between functors
df8a9782mo agoauthor_emailAdd compose_functor constructor
1aff3752mo agoauthor_emailAdd terminal category and Functor structure
4abffc63mo agoauthor_emailAdd product category construction
54b92fa3mo agoauthor_emailUpdate build artifacts
41fcc4b3mo agoauthor_emailAdd opposite category construction
756c4003mo agoauthor_emailAdd discrete category construction
08e92b23mo agoauthor_emailAdd Iso[O, M] structure for category isomorphisms
5351fd43mo agoauthor_emailAdd per-qrel kernel-quotient lifts for linear maps
66416e73mo agoauthor_emailAdd per-qrel kernel-quotient lifts for MonoidHom and AddMonoidHom
68d47f03mo agoauthor_emailAdd per-qrel kernel-quotient operation lifts for AddGroupHom, GroupHom, and RingHom
ddfe97b3mo agoauthor_emailAdd respects_mul / respects_inverse for normal subgroup relation
bc9fc323mo agoauthor_emailAdd pointwise mul/inv step lemmas for normal subgroup quotient relation
3a4c7513mo agoauthor_emailfeat: foundational normal subgroup definition and quotient relation helpers
327a8e43mo agoauthor_emailfeat: lift + and - through additive-subgroup quotient
ecfaf0a3mo agoauthor_emailfeat: subgroup quotient respects negation and addition for AddCommGroup
0a159c13mo agoauthor_emailfeat: additive-subgroup quotient relation is a congruence over AddCommGroup
7a69d853mo agoauthor_emailfeat: add foundational additive subgroup API and its quotient relation
7fba0183mo agoauthor_emailfeat: bridge linear-map kernels to additive congruence and smul preservation
3f49e1b3mo agoauthor_emailfeat: bridge ring homomorphism kernels to ring congruences
ba4588d3mo agoauthor_emailfeat: bridge MonoidHom and GroupHom kernels to multiplicative congruences
d4432803mo agoauthor_emailfeat: bridge AddGroupHom kernels to additive congruences with negation
dabbb763mo agoauthor_emailfeat: add additive monoid kernel-to-congruence bridge
3f1a8443mo agoauthor_emaildocs: record migration audit for hand-simulated quotients
f7600cf3mo agoauthor_emailfeat: add kernel relation API and quotient factorization
adb50ea3mo agoauthor_emailfeat: complete round-trip set equalities for quotient subobject transport
21d48e23mo agoauthor_emailfeat: add quotient subobject transport API
0d288be3mo agoauthor_emailfeat: add pullback/pushforward distributivity over union, intersection, converse
f99af2a3mo agoauthor_emailfeat: add compose lemmas relating single steps to refl-trans closure
faf73f93mo agoauthor_emailfeat: add step, self-composition, and converse lemmas for relation closures
367909a3mo agoauthor_emailfeat: distribute relation composition over union and intersection
046f3db3mo agoauthor_emailfeat: add equivalence closure of relations
a85be1c3mo agoauthor_emailfeat: add closure laws for transitive and reflexive-transitive closures
aa322723mo agoauthor_email