Scalar multiplication of complement

Stream: general

[Yaël Dillies]

@Eric Wieser, which way should this lemma go?

import algebra.pointwise

open_locale pointwise

variables {α β : Type*} [group α] [mul_action α β]

@[simp] lemma set.compl_smul_set (a : α) (s : set β) : (a • s)ᶜ = a • sᶜ :=
(set.image_compl_eq $ mul_action.bijective _).symm

[Yaël Dillies]

It looks like docs#neg_smul

[Eric Wieser]

I've no idea. What do we do for (-s) ᶜ?

[Yaël Dillies]

I don't think we have that docs#set.compl_neg

[Eric Wieser]

That suggests the other direction is _maybe_ better. But maybe it's just best to not mark it simp

[Johan Commelin]

I find the current version more natural. But not marking it simp is certainly a safe option.

[Johan Commelin]

At some point, we should try proof mining to see which lemmas are more often used as <- foobar than as foobar (in rw and simp, etc).

[Eric Wieser]

That's not necessarily a good indication they're backwards though, is it?

[Eric Wieser]

It's easier to find a lemma with the "simpler expression on the RHS" heuristic than the "most commonly used in this direction" heuristic

[Eric Wieser]

Of course that doesn't help here where neither side is obviously simpler

[Johan Commelin]

Eric Wieser said:

That's not necessarily a good indication they're backwards though, is it?

I would say it is a good indication but not a perfect one. There are certainly good reasons to keep a lemma in a particular direction.