mathlib3

ef74e2bd - refactor(number_theory/modular_forms/slash_actions): use the same notation everywhere (#18886)

refactor(number_theory/modular_forms/slash_actions): use the same notation everywhere (#18886) Previously we had both `f ∣[k] A` and `f ∣[k, A]` notation, this keeps only the former (on the assumption it more closely resembles the LaTeX). `f ∣[k;γ] A` is then added as notation for the more general `γ`-invariant case that the typeclass is designed around, even though that is never used. This makes `slash_action.map` the canonical spelling of slash actions, as opposed to a mix of this spelling and `modular_form.slash`. Since `modular_form.slash` is no longer canonical, all the lemmas about it are made private as they are immediately subsumed by the typeclass lemmas. Rather than defining the same local notation in each file, this now just opens the locale. This also ungeneralizes `has_zero` + `has_add` to `add_monoid`, since the extra generality is not used, and we do not have it for the (suspiciously!) analogous `distrib_mul_action`.