Zulip Chat Archive

Stream: general

Topic: suitable file for eventually_eq.smul


Rémy Degenne (Feb 17 2022 at 13:09):

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 (Feb 17 2022 at 13:12):

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 (Feb 17 2022 at 13:12):

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

Yaël Dillies (Feb 17 2022 at 13:12):

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 (Feb 17 2022 at 13:12):

Damn Eric

Eric Wieser (Feb 17 2022 at 13:13):

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

Eric Wieser (Feb 17 2022 at 13:14):

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

Eric Wieser (Feb 17 2022 at 13:15):

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

Rémy Degenne (Feb 17 2022 at 13:19):

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 (Feb 17 2022 at 13:27):

#12101

Yaël Dillies (Feb 17 2022 at 13:29):

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

Eric Wieser (Feb 17 2022 at 13:47):

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

Eric Wieser (Feb 17 2022 at 13:48):

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 (Feb 17 2022 at 15:42):

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


Last updated: Dec 20 2023 at 11:08 UTC