mathlib3
feat(analysis/calculus/fderiv/exp): derivative of `exp ℝ (A x)` in non-commutative rings
#19056
Open
Overview
Commits
15
Changes
View On GitHub

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

eric-wieser wants to merge 15 commits into master from eric-wieser/deriv-exp
eric-wieser
eric-wieser feat(analysis/calculus/fderiv/exp): deriv of `exp`
3d1d4b1d
eric-wieser wip
d2318ada
eric-wieser tidy some sorries
ba7b63ed
eric-wieser eric-wieser added WIP
eric-wieser add a hint
6c54c07a
eric-wieser
eric-wieser commented on 2023-05-21
eric-wieser
eric-wieser commented on 2023-05-21
eric-wieser slight tidy
a87c8bc9
eric-wieser wip
ec31e66f
eric-wieser Anatole's lemmas
f860d163
eric-wieser the other lemmas
8ee672d6
eric-wieser Merge remote-tracking branch 'origin/master' into eric-wieser/deriv-exp
0918be10
eric-wieser fix breakages
45b1baee
eric-wieser remove a hack
ec70f2b5
mathlib-dependent-issues-bot mathlib-dependent-issues-bot added blocked-by-other-PR
mathlib-dependent-issues-bot mathlib-dependent-issues-bot removed blocked-by-other-PR
mathlib-dependent-issues-bot
eric-wieser Merge remote-tracking branch 'origin/master' into eric-wieser/deriv-exp
36eea538
eric-wieser remove duplicate
583a6668
eric-wieser wip
5c78c939
eric-wieser eric-wieser added help-wanted
eric-wieser add a reference
685cbb0f
kim-em kim-em added too-late

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
help-wanted WIP too-late
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum