Commit 2022-07-18 15:26 903e8941

View on Github →

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.

Estimated changes