style(RingTheory): fix whitespace #30685
Conversation
Extracted from leanprover-community#30658. Found by extending the commandStart linter to proof bodies.
PR summary aa7a3d977bImport 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
|
| ((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. |
leanprover-community-mathlib4-bot
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 |
leanprover-community-mathlib4-bot
added
delegated
5 participants
Extracted from #30658. Found by extending the commandStart linter to proof bodies.