Commit 2026-07-27 20:26 c997a234

View on Github →

feat: finrank is preserved by IsFractionRing (#41694) This PR gives a direct proof of Algebra.IsAlgebraic.finrank_of_isFractionRing which avoids any additional assumptions beyond those required for the statement (including Algebra.IsAlgebraic).

Estimated changes