Stream: general

Topic: Fishy instance finding

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.

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