Floris van Doorn
Floris van Doorn
feat(analysis/calculus/cont_diff): Prove that `fderiv_within` is `C^n` for functions with parameters
> Is it hard to split this PR into 2: (1) reorder/rename; (2) new features? Ok, I opened #17585, which can be merged first
feat(analysis/calculus/cont_diff): Prove that `fderiv_within` is `C^n` for functions with parameters
oops, I did that request before I saw the latest review. Thanks for the initial review! EDIT: but now it can be reviewed again :-)
feat(analysis/calculus/cont_diff): Prove that `fderiv_within` is `C^n` for functions with parameters
Thanks for the synchronization reminder, I might have forgotten it. It is leanprover/mathlib4#1833
feat(analysis/calculus/cont_diff): Prove that `fderiv_within` is `C^n` for functions with parameters
bors merge
True. That is not visible on the `/seed/...` page though.
The regressions in Mathlib seem very similar to the issue reported in #2736. Is this change in Lean actually an improvement? Do you know what causes the current `rw` to...
Oh, shift-click on the green + button is great! That already resolves most of this issue (and saves two clicks compared to my first two suggestions). I never considered reading...
I got the same error on version 1.1.78. Here are steps to reproduce: 1. In a new game, make a new factory for iron chests, and make it using its...
I just want to say that I'm still eagerly awaiting a relaunch of this project. I haven't found a way to manage my youtube subscriptions nearly as well as sanegrid...
Another one: [WfDvdMonoid](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/UniqueFactorizationDomain.html#WfDvdMonoid)[WfDvdMonoid](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/UniqueFactorizationDomain.html#WfDvdMonoid) not hyperlinking `DvdNotUnit`