finsupp.nonzero_iff_exist

Stream: Is there code for X?

[Scott Morrison]

We have finsupp.nonzero_iff_exists {f : α →₀ M} : f ≠ 0 ↔ ∃ a : α, f a ≠ 0, but I'm not finding the analogue of this that I want, for linear maps. Are these hiding somewhere under a different name, or do they need adding?

[Yaël Dillies]

I just added something similar. docs#continuous_linear_map.exists_ne_zero

[Johan Commelin]

Shouldn't we just have that for arbitrary functions?

[Yaël Dillies]

Well, yeah, but it depends on the specific has_zero instance.

[Scott Morrison]

If we just write it for "bare" functions, we won't be able to use it with rw or simp, unfortunately.

[Yaël Dillies]

Usually, ⇑0 = 0 is defeq though.

[Scott Morrison]

Still, syntactic form is what counts. :-(

[Yaël Dillies]

@Anne Baanen, didn't you have plans to write a has_pointwise_zero instance? :grinning:

[Yaël Dillies]

You can rw [←coe_zero, coe_inj] I believe, Scott. But I agree it's a pain.

[Scott Morrison]

But I don't want to have extra rewrites, or to have to know a silly name like coe_zero. :-)

[Scott Morrison]

and library_search must find this lemma

[Scott Morrison]

because otherwise I'm going to have to ask here again. :-)

[Yaël Dillies]

I'm always here to serve!

[Eric Wieser]

Shouldn't we just have that for arbitrary functions?

docs#function.ne_iff

[Eric Wieser]

docs#fun_like.ne_iff

[Eric Wieser]

Zero falls out as an uninteresting special case, since pretty much all function types have 0 x = 0 by definition

[Anne Baanen]

Yaël Dillies said:

Anne Baanen, didn't you have plan,s to write a has_pointwise_zero instance? :grinning:

I don't recall that. Wasn't Yury doing something with pointwise maps?

[Scott Morrison]

The other similiar statement I'd like is nontrivial iff surjective f → f ≠ 0. That seems harder to make polymorphic, because of the "what does the zero function mean" issue.

[Eric Wieser]

You could always put a coe_fn on the f

[Eric Wieser]

Which I guess would be on all occurences of f at that point, so it just becomes about function.

[Eric Wieser]

What I think we are missing are lemmas like docs#linear_map.coe_eq_zero which should contain the obvious iff

[Yaël Dillies]

Yeah I proved some stuff similar to that a while back. See docs#finset.coe_eq_singleton. This dumb lemma is super practical.