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

feat(analysis/calculus/fderiv/exp): derivative of exp ℝ (A x) in non-commutative rings #19056

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

feat(analysis/calculus/fderiv/exp): derivative of exp ℝ (A x) in non-commutative rings #19056

wants to merge 15 commits into from

Commits on May 21, 2023

  1. feat(analysis/calculus/fderiv/exp): deriv of exp

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

  2. wip

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

  3. tidy some sorries

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

  4. add a hint

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

  5. slight tidy

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

Commits on May 22, 2023

  1. wip

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

  2. Anatole's lemmas

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

  3. the other lemmas

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

  4. Merge remote-tracking branch 'origin/master' into eric-wieser/deriv-exp

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

  5. fix breakages

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

  6. remove a hack

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

Commits on May 26, 2023

  1. Merge remote-tracking branch 'origin/master' into eric-wieser/deriv-exp

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

  2. remove duplicate

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

  3. wip

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

  4. add a reference

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