Theorem Subalgebra.isIntegral_iff

Modification history

2025-11-05 21:07
Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean
chore(RingTheory/IntegralClosure/Algebra/Basic): relax unnecessary commutativity assumption (#31297) …
Modified Subalgebra.isIntegral_iffView on Github →
2024-10-17 11:36
Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean
feat(Algebra): integralClosure as IntermediateField (#14206) …
Added Subalgebra.isIntegral_iffView on Github →