OAI/Combinatorics/Progressions/Geometry/NativeMixedCoordinateSlices.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.mixedInputCoordinate line 9
2. def OAI.Erdos3.mixedCoordinateIndex line 12
3. theorem OAI.Erdos3.mixedInputCoordinate_index line 15
4. theorem OAI.Erdos3.mixedInputCoordinate_eval line 21
5. theorem OAI.Erdos3.mixedExchangeCoordinate_involutive line 29
6. theorem OAI.Erdos3.mixedExchangeCoordinate_update line 36
7. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixed_frozen_affine_expansion line 69
8. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixed_scalar_coordinate_slice line 109
9. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixed_kernel_coordinate_slice line 137