Yury G. Kudryashov
Yury G. Kudryashov
Yes, in the code. BTW, what lemmas does lean4 calc mode use? In lean 3 we had one attribute that was used both for calc and trans. In lean 3,...
When you want another round of review, you remove awaiting author and add awaiting review.
One more bug in `calc`: ```lean import data.set.basic example (α : Type*) (x : α) (s t t' : set α) (hx : x ∈ s) (h : s ⊆...
Please split this into smaller PRs. E.g., I see that you have a `prod.measure_space` instance. This definitely can (and should) be a separate PR. This way (a) some chunks will...
`stump-learnable` is under the same Apache 2.0 license, so you may PR code from that repo without asking the authors as long as you preserve their copyrights. It's pretty clear...
Please remove the commented code, move lemmas to appropriate files, and use `to_additive` to generate lemmas about `is_add_fundamental_domain` when possible. Also see #17293 for a version of `exists_mul_inv_mem_lattice_of_volume_lt_volume`.
IMHO, a 300+ lines long PR deserves a longer commit message.
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?
> This currently contains your review of "cubing the cube". Did some rebase go wrong? No, I touched API about `2 ≤ cardinal.mk α`, this broke `cubing_a_cube`, so I migrated...
@jcommelin Merged master.