Commit 2025-07-04 20:53 4dca3663

View on Github →

chore: remove noncomputable from Set/Finset Monoid instances (#26755)

Estimated changes

Modified Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean

added def Finset.coeMonoidHom

Modified Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

added def Set.singletonMonoidHom

added def Set.singletonMulHom

added def Set.singletonOneHom