Commit 2022-08-24 09:35 214f197b

View on Github →

refactor(field_theory/*): Move and golf alg_hom.fintype (#16114) This PR moves alg_hom.fintype to minpoly.lean so that it can be used later (e.g., in normal.lean).

Estimated changes

Modified src/field_theory/fixed.lean

deleted theorem aux_inj_roots_of_min_poly

Modified src/field_theory/minpoly.lean

added theorem minpoly.aux_inj_roots_of_min_poly