OAI/Analysis/InterpolatedFactors/InverseRecognition.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FreeGroupFactorMain.GaussianRecognition.System.generatedIso_symm_normal line 17
2. theorem OAI.FreeGroupFactorMain.FullReducingCorner.restrictionIso_symm_normal line 35
3. theorem OAI.FreeGroupFactorMain.GaussianRecognition.System.fullReductionIso_symm_normal line 60
4. theorem OAI.FreeGroupFactorMain.WeightedFock.reducedGaussianIso_symm_normal line 79
5. theorem OAI.FreeGroupFactorMain.WeightedFock.fullGaussianIso_symm_normal line 86
6. theorem OAI.FreeGroupFactorMain.WeightedFock.ambientGaussianIso_symm_normal line 100