Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-26 12:10 3443a7d4

View on Github →

feat(analysis/complex/basic): restriction of scalars, real differentiability of complex functions (#1716)

  • restrict scalar
  • staging
  • complete proof
  • staging
  • cleanup
  • staging
  • cleanup
  • docstring
  • docstring
  • reviewer's comments
  • Update src/analysis/complex/basic.lean Co-Authored-By: Rob Lewis Rob.y.lewis@gmail.com
  • Update src/analysis/calculus/fderiv.lean Co-Authored-By: Rob Lewis Rob.y.lewis@gmail.com
  • add ! in docstrings [ci skip]
  • more doc formatting in fderiv
  • fix comments
  • add docstrings

Estimated changes