What's with the `_` in `zero_`?

Stream: maths

[Kevin Buzzard]

I've seen this in a few places now:

class is_submodule {α : Type u} {β : Type v} [ring α] [module α β] (p : set β) : Prop :=
(zero_ : (0:β) ∈ p)
(add_  : ∀ {x y}, x ∈ p → y ∈ p → x + y ∈ p)
(smul : ∀ c {x}, x ∈ p → c • x ∈ p)

Why zero_ and add_ but not smul_?

[Mario Carneiro]

I think we are using ' for this now

[Mario Carneiro]

it's avoiding a name clash with a restated axiom just below it

[Kevin Buzzard]

Once we decide on a convention will it mean that a lot of code needs to be rewritten? The idea is that we are separating off the actual constructor (which is supposed to be thought of as hidden?) from the user interface? Of course ' is used in other situations in mathlib to mean something else -- like "oh if you don't want that add_sub_cancel you might instead find add_sub_cancel' useful", right?