Syntax idiomatic definition class

Stream: mathlib4

[Martin Dvořák]

Which of the following syntaxes is idiomatic in the definition of an algebraic class please?

(1)

mul_smul : ∀ x y : α, ∀ b : β, (x * y) • b = x • y • b

(2)

mul_smul : ∀ (x y : α) (b : β), (x * y) • b = x • y • b

(3)

mul_smul (x y : α) (b : β) : (x * y) • b = x • y • b

[Ruben Van de Velde]

Last one is best, imo

[Aaron Liu]

I like the last one best but not to the extent that I would change it in existing code