Commit 2026-01-23 09:36 fda9589a

View on Github →

chore(Algebra/Group/Submonoid): golf Nat.addSubmonoidClosure_one using simp (#27785) This should improve the proof readability.

Estimated changes