Commit 2026-03-23 14:33 34ea11a4

View on Github →

chore(RingTheory/IntegralDomain): review file (#36117) This PR does the following:

  • rename two theorems to better match Mathlib standards
  • golf a proof

Estimated changes