DistribSMul instance for NonAssocNonUnitalRing

Stream: Is there code for X?

[Scott Carnahan]

Does something like:

instance instNameHere [NonUnitalNonAssocSemiring R] : DistribSMul R R where smul_add := mul_add

cause any problems?
If it's okay, is there a good place to put it? #find_home only suggested the file I was working on.

[Damiano Testa]

You could try #find_home! for a possibly better suggestion.

[Damiano Testa]

(I am not sure about the other questions that you asked.)

[Eric Wieser]

That instance looks fine to me

[Eric Rodriguez]

Can there ever be any problems with Prop instances? And yes, find_home currently doesn't work with things that create auxiliary declarations in the background

[Yaël Dillies]

This is not a Prop-valued instance, though

[Eric Rodriguez]

Ah, I forget it's not a mixin

[Damiano Testa]

Are you sure about find_home? I thought that I fixed that with the #find_home! syntax...

[Eric Rodriguez]

I wasn't aware of find_home!

[Scott Carnahan]

#find_home! worked!

[Scott Carnahan]

Answer: Mathlib.Algebra.SMulWithZero

[Damiano Testa]

Great! What find_home! should do is to compute the same sup of the imports, but removing the current file from the set of imports before the sup step. The sup could still be the current file, but in that case it should be meaningful!

[Scott Carnahan]

It's a bit surprising, since neither NonUnitalNonAssocSemiring nor DistribSMul appear in the file. I guess the Mathlib.Algebra.Ring.Opposite import brings in the ring theory.

[Damiano Testa]

It is also possible that there are other bugs in find_home...

[Scott Carnahan]

Thanks for your input!
#10162

[Damiano Testa]

I took the liberty of adding an extra white line to separate the text and the --- from the PR description, for what I think is the intended formatting!

[Scott Carnahan]

Thank you! I was wondering how to get rid of the boldface type.

[Damiano Testa]

I think that it is a markdown "feature": text around --- is subject to be interpreted as a header.