Commit 2026-03-18 16:07 59cb29bd

View on Github →

chore(IsFractionRing): make argument explicit (#36655) Makes the base ring an explicit argument in IsFractionRing.div_surjective. This argument cannot be inferred by typeclass inference, because the base ring is not an outParam or semiOutParam in the type of IsFractionRing. It is also rarely determined by the expected type, since this is typically used as the discriminant for an obtain or rcases. Also update every usage of IsFractionRing.div_surjective to take advantage of this explicit argument.

Estimated changes