wip: make RingHom.ker and friends take in a concrete morphism instead - #43561

Open

grunweg wants to merge 10 commits into

leanprover-community:masterfrom

grunweg:ringhomker-manual

Commits on Sep 7, 2026

wip: make Ideal.map,comap take a concrete morphism
grunweg
committed
eef5d4d
Progress
grunweg
committed
8096b0f
Progress
grunweg
committed
5849b40
Microprogress
grunweg
committed
1e38902

Commits on Sep 8, 2026

Progress
grunweg
committed
4a7bf50
A few concretisations, clearly good
grunweg
committed
4a97aa5
Misc fixes
grunweg
committed
a7a63e6
One sorried proof
grunweg
committed
a37d6d8
Further clear fixes
grunweg
committed
8114c98
sorry a few more
grunweg
committed
41b9e3a