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

Modified src/algebra/algebra/subalgebra/basic.lean

added theorem algebra.range_top_iff_surjective

Modified src/ring_theory/adjoin/power_basis.lean

Modified src/ring_theory/adjoin_root.lean

added def adjoin_root.minpoly.equiv_adjoin

added theorem adjoin_root.minpoly.to_adjoin.apply_X

added theorem adjoin_root.minpoly.to_adjoin.injective

added theorem adjoin_root.minpoly.to_adjoin.surjective

added def adjoin_root.minpoly.to_adjoin

added theorem adjoin_root.minpoly.to_adjoin_apply'

added def algebra.adjoin.power_basis'