suitable file for eventually_eq.smul

Stream: general

[Rémy Degenne]

I am looking for a suitable place to put the following lemma:

lemma eventually_eq.smul {α β 𝕜} [has_scalar 𝕜 β] {l : filter α} {f f' : α → 𝕜}
  {g g' : α → β} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
  f • g =ᶠ[l] f' • g' := sorry

The other eventually_eq.*** for mul, add, and many other simple consequences of the composition rules for eventually_eq are in order/filter/basic, but the instance function.has_scalar is not available there. That instance is defined in linear_algebra.pi. It looks like that file imports a lot of things, so I'd like to avoid importing it into order/filter/basic. The question is then: where can the eventually_eq.smul lemma go?

[Eric Wieser]

docs#function.has_scalar should be moved, it was put there at the end of a long refactor to resolve a unification issue.

[Eric Wieser]

but it only really needs docs#pi.has_scalar anyway, which is available much earlier

[Yaël Dillies]

It seems the problem is that function.has_scalar is not defined as early as pi.has_mul. Can't we move it earlier?

[Yaël Dillies]

Damn Eric

[Eric Wieser]

If it makes you feel better @Yaël Dillies, it's my fault that its in the wrong place

[Eric Wieser]

docs#function.algebra is also in the wrong place, if you're looking for an easy PR

[Eric Wieser]

Both only exist in the first place because typeclass search gets confused by pi instances on non-dependent types

[Rémy Degenne]

I mentioned function.has_scalar because when I clicked on the smul icon in a file where the lemma made sense, that is what the infoview told me. But indeed, pi.has_scalar is enough, thanks! Maybe I could simply import group_theory.group_action.pi in order.filter.basic?

[Rémy Degenne]

#12101

[Yaël Dillies]

No, order theory is meant to live lower than group theory.

[Eric Wieser]

Perhaps, but order.filter.basic already talks about algebra in eventually_eq.sub etc

[Eric Wieser]

So I think where @Rémy Degenne has it is consistent with the rest of the file, even though I'm sympathetic to wanting to keep order and algebra separate for as long as possible

[Yury G. Kudryashov]

Another solution is to move eventually_eq.mul etc to a new file