Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-31 05:47 66f30901

View on Github →

feat(analysis/analytic): first take on analytic functions (#2199)

  • analytic: first definitions
  • docstrings
  • cleanup
  • Update src/analysis/analytic/basic.lean Co-Authored-By: Johan Commelin johan@commelin.net
  • comment on polydisk of convergence
  • coefficient at 0
  • protect sum
  • rename with_top.dense_coe

Estimated changes

added theorem analytic_at.add
added theorem analytic_at.neg
added theorem analytic_at.sub
added def analytic_at
added structure has_fpower_series_on_ball