mathlib

a8618391 - feat(ring_theory/discriminant): add discr_mul_is_integral_mem_adjoin (#11396)

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.