OAI/Analysis/InterpolatedFactors/CornerRepresentation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.FreeGroupFactorMain.Amplification.RangeCorner line 13
2. def OAI.FreeGroupFactorMain.Amplification.cornerRestrict line 15
3. def OAI.FreeGroupFactorMain.Amplification.cornerExtend line 18
4. theorem OAI.FreeGroupFactorMain.Amplification.cornerRestrict_extend line 28
5. theorem OAI.FreeGroupFactorMain.Amplification.cornerExtend_restrict line 33
6. theorem OAI.FreeGroupFactorMain.Amplification.cornerRestrict_apply line 38
7. def OAI.FreeGroupFactorMain.Amplification.cornerRepresentation line 43