Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

refactor(number_theory/modular_forms/slash_actions): slash actions are families of distrib_mul_actions #18932

Open
wants to merge 11 commits into
base: master
Choose a base branch
from
Open

refactor(number_theory/modular_forms/slash_actions): slash actions are families of distrib_mul_actions #18932

wants to merge 11 commits into from

Commits on Apr 27, 2023

  1. refactor: ungeneralize from has_zero has_add to add_monoid 

    The extra generality is unused, and this brings it closed to `distrib_mul_action`
    @eric-wieser
    eric-wieser committed Apr 27, 2023
    Configuration menu
    Copy the full SHA
    5ec2a32 View commit details
    Browse the repository at this point in the history

  2. wip

    @eric-wieser
    eric-wieser committed Apr 27, 2023
    Configuration menu
    Copy the full SHA
    8c339c7 View commit details
    Browse the repository at this point in the history

  3. wip

    @eric-wieser
    eric-wieser committed Apr 27, 2023
    Configuration menu
    Copy the full SHA
    92f492e View commit details
    Browse the repository at this point in the history

Commits on May 3, 2023

  1. Merge remote-tracking branch 'origin/master' into eric-wieser/slash_a… 

    …ction.redo
    @eric-wieser
    eric-wieser committed May 3, 2023
    Configuration menu
    Copy the full SHA
    042f048 View commit details
    Browse the repository at this point in the history

  2. fixes

    @eric-wieser
    eric-wieser committed May 3, 2023
    Configuration menu
    Copy the full SHA
    bf882eb View commit details
    Browse the repository at this point in the history

  3. golf

    @eric-wieser
    eric-wieser committed May 3, 2023
    Configuration menu
    Copy the full SHA
    440ccdd View commit details
    Browse the repository at this point in the history

  4. type

    @eric-wieser
    eric-wieser committed May 3, 2023
    Configuration menu
    Copy the full SHA
    41255a4 View commit details
    Browse the repository at this point in the history

  5. notation

    @eric-wieser
    eric-wieser committed May 3, 2023
    Configuration menu
    Copy the full SHA
    d1c29ed View commit details
    Browse the repository at this point in the history

  6. golf

    @eric-wieser
    eric-wieser committed May 3, 2023
    Configuration menu
    Copy the full SHA
    51ed55e View commit details
    Browse the repository at this point in the history

Commits on May 4, 2023

  1. Merge remote-tracking branch 'origin/master' into eric-wieser/slash_a… 

    …ction.redo
    @eric-wieser
    eric-wieser committed May 4, 2023
    Configuration menu
    Copy the full SHA
    25af56d View commit details
    Browse the repository at this point in the history

Commits on May 10, 2023

  1. lintfix

    @eric-wieser
    eric-wieser committed May 10, 2023
    Configuration menu
    Copy the full SHA
    bca017a View commit details
    Browse the repository at this point in the history