mathlib
738054fa - chore(number_theory/modular_forms/slash_invariant_forms): golf and rename (#18933)

Commit
2 years ago
chore(number_theory/modular_forms/slash_invariant_forms): golf and rename (#18933) In the `slash_action` namespace, this renames: * `right_action` to `slash_mul` (and reverses the direction), to match `slash_one` * `add_action` to `add_slash`, to match `zero_slash` * `smul_action` to `smul_slash`, to match `zero_slash`
Author
Parents
Loading