What does include clause do

Stream: new members

[Sebastián Galkin]

I see code in mathlib doing the following:

variables {mM : monoid M} {mN : monoid N}

include mM mN

What does include achieve exactly?

More generally? Where could I read about this type of thing? I couldn't find it on the reference manual.

[Bryan Gin-ge Chen]

See https://leanprover.github.io/theorem_proving_in_lean/interacting_with_lean.html#more-on-sections