ModuleFiniteGeneratorRankBridge.lean
Nyll.ProCGroups.ProP.FiniteGeneratorRankBridge
2 declarations indexed from sourceView source ↗ Module documentation
Finite-set presentation of topological generator rank
The LeanEval benchmark presents generator rank as the least cardinality of a finite topological generating set. For a topologically finitely generated profinite group, this agrees with the library's cardinal-valued topological rank followed by Cardinal.toNat.
Declarations
ClassFieldTower.ProP.finiteTopologicalGeneratorRank
DocumentationThe least cardinality of a finite topological generating set. This is the exact presentation used by the LeanEval trusted generatorRank helper.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.ProP
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
noncomputable section
universe u
ClassFieldTower.ProP.finiteTopologicalGeneratorRank_eq_topologicalGeneratorRank
DocumentationOn a topologically finitely generated profinite group, the finite-set presentation and the library topological generator rank coincide.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.ProP
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
noncomputable section
universe u