NYLL
Module

Framework.lean

Nyll.ProCGroups.FreeConstructions.Framework
1 declaration indexed from sourceView source ↗

Module documentation

Finite generating data

This file records concrete finite generating maps and finite families of subgroups. The companion bounds concatenate those maps to obtain explicit generating families for the ambient group.

Imports1
Imported by2

Declarations

def

AbstractGeneratorRankLE

L24 ↗
ProCGroups.FreeConstructions.AbstractGeneratorRankLE
Documentation

The group is generated by at most \(r\) elements, expressed by an actual generating map.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
namespace ProCGroups.FreeConstructions
Lean source · statement
def AbstractGeneratorRankLE (G : Type u) [Group G] (r : Nat) : Prop

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.