Main result
The proof packages a polynomial composition criterion through generic-fiber relations, splitting fields, Frobenius descent steps, and a cubic square-root functional-equation specialization.
- Contribution type
- New viewpoint; Lean formalization
- Contribution
- Galois-descent and Frobenius-reduction viewpoint on a separated-polynomial composition criterion, including a Lean-checked cubic square-root functional equation.
- Mechanism
- generic fibers, Galois descent, Frobenius reduction
- Lean theorem family
SeparatedComposition.separated_composition_criterion_iff- Lean and mathlib
- Lean 4.30.0-rc2, mathlib v4.30.0-rc2
- Build command
lake build