OAI/Analysis/JiangSu/DimensionDrop/DimensionDropPureFibres.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DimensionDropRelations.Witness.map line 19
2. lemma OAI.DimensionDropRelations.Witness.map_parameter line 27
3. def OAI.DimensionDropRelations.Witness.generators line 31
4. def OAI.DimensionDropRelations.Witness.generated line 32
5. lemma OAI.DimensionDropRelations.Witness.parameter_commute_generated line 34
6. theorem OAI.DimensionDropRelations.Witness.pure_scalar_coordinate line 59