Commit 2025-07-04 15:57 c6f4e126

chore: remove unnecessary noncomputable attribute (#26747) This is no longer necessary after updating to 4.22 with the new compiler. The other remaining noncomputable from the same adaptation note on Finset.addMonoid is still required, because that definition applies Injective.addMonoid to the noncomputable Set.addMonoid.