Commit 2020-11-05 18:57 a12d6772

feat(ring_theory): define a power_basis structure (#4905) This PR defines a structure power_basis. If S is an R-algebra, pb : power_basis R S states that S (as R-module) has basis 1, pb.gen, ..., pb.gen ^ (pb.dim - 1). Since there are multiple possible choices, I decided to not make it a typeclass. Three constructors for power_basis are included: algebra.adjoin, intermediate_field.adjoin and adjoin_root. Each of these is of the form power_basis K _ with K a field, at least until minimal_polynomial gets better support for rings.