mathlib3

903e8941 - feat(ring_theory/adjoin_root): add lemmas for GCD domains (#14981)

feat(ring_theory/adjoin_root): add lemmas for GCD domains (#14981) We add `algebra.adjoin.power_basis'` and `power_basis.of_gen_mem_adjoin'`, that generalize the umprimed versions to GCD domain. From flt-regular.