Commit 2024-09-16 17:23 007dfdef

View on Github →

feat: more API for AnalyticWithinAt (#16843) The PR adds versions for AnalyticWithinAt of many lemmas that were already available for AnalyticAt (and sometimes deduces the AnalyticAt versions from the AnalyticWithinAt). It is a little long, but mostly trivial without any real mathematical content.

Estimated changes

added theorem AnalyticWithinAt.add
added theorem AnalyticWithinAt.neg
added theorem AnalyticWithinAt.sub
added theorem AnalyticWithinOn.add
added theorem AnalyticWithinOn.neg
added theorem AnalyticWithinOn.sub
added theorem analyticWithinAt_const
added theorem analyticWithinOn_const
added theorem AnalyticWithinAt.div
added theorem AnalyticWithinAt.inv
added theorem AnalyticWithinAt.mul
added theorem AnalyticWithinAt.pow
added theorem AnalyticWithinAt.prod
added theorem AnalyticWithinAt.smul
added theorem AnalyticWithinOn.div
added theorem AnalyticWithinOn.inv
added theorem AnalyticWithinOn.mul
added theorem AnalyticWithinOn.pow
added theorem AnalyticWithinOn.prod
added theorem AnalyticWithinOn.smul
added theorem analyticAt_pi_iff
added theorem analyticOn_pi_iff
modified theorem analyticAt_fst
modified theorem analyticAt_id
modified theorem analyticAt_snd
modified theorem analyticOn_fst
modified theorem analyticOn_id
modified theorem analyticOn_snd
added theorem analyticWithinAt_fst
added theorem analyticWithinAt_id
added theorem analyticWithinAt_snd
added theorem analyticWithinOn_fst
added theorem analyticWithinOn_id
added theorem analyticWithinOn_snd
modified theorem MeromorphicAt.id
deleted theorem AnalyticWithinAt.prod
deleted theorem AnalyticWithinOn.prod