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