mathlib3
feat(analysis/calculus/fderiv/exp): derivative of `exp ℝ (A x)` in non-commutative rings
#19056
Open
Overview
Commits
15
Changes
View On GitHub
Commits
  • feat(analysis/calculus/fderiv/exp): deriv of `exp`
    eric-wieser committed 3 years ago
  • wip
    eric-wieser committed 3 years ago
  • tidy some sorries
    eric-wieser committed 3 years ago
  • add a hint
    eric-wieser committed 3 years ago
  • slight tidy
    eric-wieser committed 3 years ago
  • wip
    eric-wieser committed 3 years ago
  • Anatole's lemmas
    eric-wieser committed 3 years ago
  • the other lemmas
    eric-wieser committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into eric-wieser/deriv-exp
    eric-wieser committed 3 years ago
  • fix breakages
    eric-wieser committed 3 years ago
  • remove a hack
    eric-wieser committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into eric-wieser/deriv-exp
    eric-wieser committed 3 years ago
  • remove duplicate
    eric-wieser committed 3 years ago
  • wip
    eric-wieser committed 3 years ago
  • add a reference
    eric-wieser committed 3 years ago
FAQ Terms Privacy Refunds Impressum
Loading