OAI/Geometry/HeilbronnTriangle/RealPlaneReduction.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem355.RealPlaneReduction.kernelEquiv line 12
2. def OAI.Problem355.RealPlaneReduction.reductionHom line 16
3. theorem OAI.Problem355.RealPlaneReduction.reductionHom_surjective line 21
4. theorem OAI.Problem355.RealPlaneReduction.reductionHom_kernelEquiv line 28
5. theorem OAI.Problem355.RealPlaneReduction.cast_kernelEquiv_symm line 34
6. theorem OAI.Problem355.RealPlaneReduction.line_preimage_index line 42
7. def OAI.Problem355.RealPlaneReduction.equalCoordinateLattice line 52
8. theorem OAI.Problem355.RealPlaneReduction.mem_equalCoordinateLattice line 58
9. theorem OAI.Problem355.RealPlaneReduction.equalCoordinateLattice_index line 69