Theorem Algebra.finite_adjoin_of_finite_of_isIntegral

Modification history

2025-01-27 09:35
Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean
feat(RingTheory/IntegralClosure): prove `Module.Finite R (adjoin R S)` for finite set `S` of integral elements (#20970) …
Added Algebra.finite_adjoin_of_finite_of_isIntegralView on Github →