Zulip Chat Archive

Stream: general

Topic: Fishy instance finding

view this post on Zulip Yaël Dillies (Apr 15 2021 at 05:55):

I found there's something funny going on with continuous_linear_map.map_smul.
The following code throws an error asking for semiring (E →L[ℝ] ℝ)

import tactic
import data.real.basic
import algebra.module.linear_map
import analysis.convex.topology

variables {E : Type*} [normed_group E] [normed_space  E]

lemma triv (l : E L[] ) (a : ) (x : E) :
  l (a  x) = a  l x :=
by rw l.map_smul

while this works fine:

lemma triv (l : E L[] ) (a : ) (x : E) :
  l (a  x) = a  l x :=
by rw l.map_smul _

l.map_smul_of_tower and l.map_smul' too throw peculiar instance requirements. I don't know if it's related, but I found that

theorem continuous_linear_map.map_smul {R : Type u_1} [semiring R] {M : Type u_2}
  [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂]
  [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (c : R) (f : M L[R] M₂) (x : M) :
f (c  x) = c  f x

had a weird argument order given the dot notation. I would have expected f to come before c.

view this post on Zulip Shing Tak Lam (Apr 15 2021 at 06:44):

I've only tried it on your example, but it seems like changing the order of c and f in continuous_linear_map.map_smul makes it work without needing the _.

Last updated: May 08 2021 at 09:11 UTC