Commit 2023-05-02 01:48 ef74e2bd

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.