Commit 2025-11-05 21:07 7756875c

View on Github →

chore(RingTheory/IntegralClosure/Algebra/Basic): relax unnecessary commutativity assumption (#31297)

  • Relax typeclass assumption in Subalgebra.isIntegral_iff from CommRing to Ring

Estimated changes

modified theorem Subalgebra.isIntegral_iff