Commit 2022-01-14 10:58 a8618391

feat(ring_theory/discriminant): add discr_mul_is_integral_mem_adjoin (#11396) We add discr_mul_is_integral_mem_adjoin: let K be the fraction field of an integrally closed domain R and let L be a finite separable extension of K. Let B : power_basis K L be such that is_integral R B.gen. Then for all z : L that are integral over R, we have (discr K B.basis) • z ∈ adjoin R ({B.gen} : set L). From flt-regular.