Irredundant bases for finite almost simple groups (Lean code)
收藏DataCite Commons2025-10-29 更新2026-05-07 收录
下载链接：
https://research-portal.st-andrews.ac.uk/en/datasets/25f5d93d-96fb-4569-b7f1-215aa6075dc8
下载链接
链接失效反馈官方服务：
资源简介：
This is the Lean code accompanying Peiran Wu's PhD thesis "Irredundant bases for finite almost simple groups".
The code formalises Lemma 3.15 as "mlii_eq_of_subsingleton_fixedPoints_stabilizer", which states the exact maximum irredundant base size of a wreath product H wr K in faithful product action, provided each point stabiliser in H has a single fixed point.
提供机构：
University of St Andrews
创建时间：
2025-10-29
