mathlib
74e23d34 - refactor(ring_theory/perfection): faster proof of `coeff_frobenius`

Commit

4 years ago

refactor(ring_theory/perfection): faster proof of `coeff_frobenius` 4X smaller proof term elaboration 800ms -> 50ms Co-authors: `lean-gptf`, Stanislas Polu

References

coeff_frobenius

Author

Jesse Michael Han

Parents

69bf4840

mathlib 74e23d34 - refactor(ring_theory/perfection): faster proof of `coeff_frobenius`

mathlib
74e23d34 - refactor(ring_theory/perfection): faster proof of `coeff_frobenius`