Theorem Algebra.finite_adjoin_simple_of_isIntegral

Modification history

2025-10-01 10:39
Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean
feat(RingTheory): units are exactly non-zerodivisors in noncommutative Artinian rings (#28887)
Modified Algebra.finite_adjoin_simple_of_isIntegralView on Github →
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_simple_of_isIntegralView on Github →