Documentation

LeanPool.ConnesRigidity.Foundation.GroupTheory.SpecialLinear.ElementaryGeneration

Elementary generation for Zhou §4 #

source
noncomputable def Connes.SpecialLinear.elementarySubgroup :
Subgroup SL3

The subgroup generated by elementary transvections. Paper: §4.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Connes.SpecialLinear.elementarySubgroup_eq_top :
    elementarySubgroup = ⊤

    The elementary subgroup is all of SL₃(R). Paper: §4, Proposition 4.1(a).