Context
CompPoly/Fields/Binary/Tower/Impl.lean includes a TODO near concreteTowerAlgebraMap:
migrate to Fin.dfoldl
Proposed work
- Refactor
concreteTowerAlgebraMap to use Fin.dfoldl.
- Preserve behavior and external API.
Acceptance criteria
- No API changes are required at call sites.
- proofs and/or tests to show correctness
Context
CompPoly/Fields/Binary/Tower/Impl.lean includes a TODO near
concreteTowerAlgebraMap:Proposed work
concreteTowerAlgebraMapto useFin.dfoldl.Acceptance criteria