chore(MonoidHom): make definitions taking `MonoidHom` instead `MonoidHomClass` - #43611

Open

grunweg wants to merge 50 commits into

leanprover-community:masterfrom

grunweg:concretise-submonoid

Commits on Sep 9, 2026

chore: use variables a little more
grunweg
committed
df129c4
Slightly more
grunweg
committed
d2c7065
wip
grunweg
committed
781a3ac
First batch of changes
grunweg
committed
c399b0b
Another: overall, change Submonoid.map,comap,mker and mrange (and perhaps more
grunweg
committed
d72340e
Fixes
grunweg
committed
64e69f7
Fix
grunweg
committed
3bdf8c6
Fix one proof, and generalise a lemma in the process
grunweg
committed
a3d0c6d
Fix
grunweg
committed
de0a845
Fix
grunweg
committed
1e14592
More fixes
grunweg
committed
2db0efc
Sorry a few proofs
grunweg
committed
8acbdab
More good fixes
grunweg
committed
e81b9c2
TEMP: sorry a number of broken proofs
grunweg
committed
e0bdff4
Some more good changes
grunweg
committed
0ed54f9
Mixed changes: partial fixes, partially sorry
grunweg
committed
b6ccea3
A few easy ones
grunweg
committed
b21d40d
A few more proofs; uncomment two lemmas again
grunweg
committed
6f7ca7a
Five more
grunweg
committed
b19d83f

Commits on Sep 10, 2026

remove 1 sorry
jjdishere
committed
1a71124
some progress
jjdishere
committed
0958c18
some more
jjdishere
committed
84377fd
some more
jjdishere
committed
66dd67c
more MonoidHomClass.toMonoidHom
jjdishere
committed
b0039da
final sorries
jjdishere
committed
a494dfc
build
jjdishere
committed
1201efd

Commits on Sep 23, 2026

remove doc
jjdishere
committed
464cad6
Merge branch 'master' into pr/43611
jjdishere
committed
8aaf433

Commits on Sep 24, 2026

fix
jjdishere
committed
33ebf86
fix part
jjdishere
committed
a9b05a4
fix and normalize to coe
jjdishere
committed
8c6fdb2
more normalization to coe
jjdishere
committed
75d3ad0
fix all
jjdishere
committed
fbbd458
Merge remote-tracking branch 'upstream/master' into pr/43611
jjdishere
committed
0451008
Update Membership.lean
jjdishere
committed
0cafac0
build
jjdishere
committed
4dcba20
normalize all current
jjdishere
committed
ce16773
more def refactor
jjdishere
committed
1c568d4
concrete more
jjdishere
committed
98081f9
fix
jjdishere
committed
597359c
remove a simps
jjdishere
committed
da1f902
Apply batched suggestions from code review

jjdishere
and
themathqueen
authored
1d8ec6c
fix
jjdishere
committed
4130843

Commits on Sep 25, 2026

apply suggestions
jjdishere
committed
144b8a2
fix
jjdishere
committed
ad6e392
fix more
jjdishere
committed
108fa26
fix all
jjdishere
committed
546977b
deprecate
jjdishere
committed
9764b9a

Commits on Sep 26, 2026

Merge remote-tracking branch 'upstream/master' into pr/43611
jjdishere
committed
0067ea8
fix
jjdishere
committed
e34c4d3