coe_add vs add_coe

Stream: maths

[Nicolò Cavalleri]

What is the rule to decide if to name a lemma coe_add or add_coe?

[Eric Wieser]

The naming guide says lemmas about foo (bar x y) = ... should be called foo_bar

[Eric Wieser]

So coe_add would by that scheme be coe (a + b) = ... while add_coe would be coe a + coe b = ...

[Eric Wieser]

#naming

[Eric Wieser]

Although now that I look, I can't find that rule there...

[Mario Carneiro]

I think the latter would be called coe_add_coe

[Mario Carneiro]

add_coe would be something like a + coe b = ...

[Eric Rodriguez]

but then what would coe a + b be? I would've assumed coe_add

[Eric Wieser]

Right, the naming is ambiguous. This comes up for (-a) * b = ... vs a * -b = ... vs -(a * b) = ..., although the lemma names we choose for those are an awful mouthful

[Kevin Buzzard]

I bet coe a + b is much rarer in practice than examples where a and b have the same type