!4#3332 Topology.ContinuousFunction.Algebra

Stream: mathlib4

[Eric Wieser]

This one is running into really nasty typeclass issues on what ought to be a very simple problem; it doesn't like x - y at all, where x y : s and s : Subalgebra K C(X,K)...

[Eric Wieser]

I was able to really painfully steer it to an instance, but now it appears the simp lemmas can't find the instances instead

[Eric Wieser]

Bizarrely I also think I remember simp claiming that it couldn't find a SMulMemClass instance, which is weird given I didn't ask it to find one (the instance seemed to genuinely be missing)

[Jireh Loreaux]

It's quite possible SMulMemClass instances are honestly missing. I only add that class a while ago and haven't yet thoroughly gone through and added the instances that should exist. Note that there is also SubmoduleClass.

[Eric Wieser]

What's the purpose of docs#submodule_class?

[Jireh Loreaux]

Ah, yes, I guess that looks really weird. It was originally written as extending smul_mem_class and add_submonoid_class but that ran into nasty timeouts and Anne suggested unbundling, which worked, but I didn't consider how silly that is at the time.

[Eric Wieser]

Is that a vote in favor of removing it?

[Eric Wieser]

#18902

[Eric Wieser]

Forward-ported as !4#3770

[Jireh Loreaux]

Thanks for taking care of this @Eric Wieser