{"id":"palomar/PALOMAR-2026-09-30-000037","url":"https://github.com/laurentbartholdi/hopfamenability/tree/6399798618014ed9a89694008cceb5b75707c7e0","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-30-000037-v1.json","repo":"https://github.com/laurentbartholdi/hopfamenability","tags":["math.RA","math.GR","msc:16T05","msc:43A07","amenability","hopf-algebras","group-theory","formalization"],"score":0,"title":"Amenability of Lie, group and Hopf algebras","trust":"high","domain":"math.RA","source":"palomar","authors":["Laurent Bartholdi"],"reviews":0,"subject":"math.RA","summary":"Formalization of 18 claims from manuscript Theorems A, B, C, E (extension direction), F, G, H (hierarchy inclusions and characteristic-zero strictness), I, and J. The claims include coalgebraic rounding, algebraic and coalgebraic amenability, Hopf-module quotients, cleft extensions, group and Lie applications, and augmentation-associated graded amenability. Every selected claim is proved without unformalized literature inputs or project-local axioms. Theorem D, the equivalence form of E, and arbitrary-characteristic strictness in H remain in the library but are excluded from the submission.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-30","reactions":{},"formalized":true,"formalizes":[{"title":"Amenability of Lie, Group and Hopf algebras","identifier":"https://arxiv.org/abs/2609.10373v1","relationship":"formalizes"}]}