[Merged by Bors] - style(RingTheory): fix whitespace#30685
[Merged by Bors] - style(RingTheory): fix whitespace#30685grunweg wants to merge 4 commits intoleanprover-community:masterfrom
Conversation
Extracted from leanprover-community#30658. Found by extending the commandStart linter to proof bodies.
PR summary 3218e4a7b1Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
chrisflav
left a comment
chrisflav
left a comment
There was a problem hiding this comment.
LGTM, modulo the factorial notation.
maintainer delegate
| ((j ! : ℚ)⁻¹ * ((i - j) ! : ℚ)⁻¹) • (a ^ j * b ^ (i - j))) := ?_ | ||
| ((j ! : ℚ)⁻¹ * ((i - j)! : ℚ)⁻¹) • (a ^ j * b ^ (i - j))) := ?_ | ||
| _ = ∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N, | ||
| ((ij.1 ! : ℚ)⁻¹ * (ij.2 ! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2) := ?_ | ||
| ((ij.1! : ℚ)⁻¹ * (ij.2! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2) := ?_ |
There was a problem hiding this comment.
This seems inconsistent with space before ! or not. Similarly below.
There was a problem hiding this comment.
I agree, let's just postpone this to the moment we will be able to write n! (or at least the moment we will be able to make a final choice).
|
🚀 Pull request has been placed on the maintainer queue by chrisflav. |
ghost
added
the
maintainer-merge
| ((j ! : ℚ)⁻¹ * ((i - j) ! : ℚ)⁻¹) • (a ^ j * b ^ (i - j))) := ?_ | ||
| ((j ! : ℚ)⁻¹ * ((i - j)! : ℚ)⁻¹) • (a ^ j * b ^ (i - j))) := ?_ | ||
| _ = ∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N, | ||
| ((ij.1 ! : ℚ)⁻¹ * (ij.2 ! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2) := ?_ | ||
| ((ij.1! : ℚ)⁻¹ * (ij.2! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2) := ?_ |
There was a problem hiding this comment.
I agree, let's just postpone this to the moment we will be able to write n! (or at least the moment we will be able to make a final choice).
|
✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with |
ghost
added
delegated
|
Thanks for the careful review! |
Extracted from #30658. Found by extending the commandStart linter to proof bodies. Co-authored-by: adomani <adomani@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Extracted from leanprover-community#30658. Found by extending the commandStart linter to proof bodies. Co-authored-by: adomani <adomani@gmail.com>
Extracted from leanprover-community#30658. Found by extending the commandStart linter to proof bodies. Co-authored-by: adomani <adomani@gmail.com>
4 participants
Extracted from #30658. Found by extending the commandStart linter to proof bodies.