Commit 2025-02-26 15:48 b973ae78
View on Github →feat(Algebra/Module): the minimum cardinality of generating set (#20744)
In this PR, we ported a part of Andrew Yang's lean3 repository at this repository, which is appoved by @erdOne after his discussion with @chrisflav.
Andrew defined min_generator_card and spanrank in this repository (it's at /dimension_theory/min_generator_card), we ported this, and ported some basic lemmas about it.
@erdOne
@xyzw12345 wangjt2020@163.com
@jjdishere emailboxofjjd@163.com
@Blackfeather007 2100017455@stu.pku.edu.cn