27. HexBerlekampZassenhaus: factorization over the integers🔗

1. 27.1. From integer factors to modular factors
2. 27.2. Direct integer coordinates
3. 27.3. Classical recombination
4. 27.4. Iterated quadratic norms
5. 27.5. Logarithmic derivatives and lattice recombination
6. 27.6. Small lattices as checked proposals
7. 27.7. Prime choice and totality
8. 27.8. Result and correctness
9. 27.9. The Mathlib correspondence
10. 27.10. Relationship to the tactics