We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent c3a1102 commit 3550579Copy full SHA for 3550579
1 file changed
Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Extremal.lean
@@ -19,8 +19,8 @@ following proof in https://math.stackexchange.com/a/978145/1277
19
20
## Main statements
21
22
-* `leadingCoeff_le_of_bounded`: If P is a degree n polynomial and |P(x)|≤1 for all |x|≤1 then
23
- the leading coefficient of P is at most 2^(n-1)
+* leadingCoeff_le_of_bounded: If `P` is a degree `n` real polynomial and `|P (x)| ≤ 1` for all `|x| ≤ 1` then
+ the leading coefficient of `P` is at most `2 ^ (n-1)`
24
* `leadingCoeff_eq_iff_of_bounded`: If P is a degree n polynomial and |P(x)|≤1 for all |x|≤1 then
25
the leading coefficient of P equals 2^(n-1) iff P = T_n, the n'th Chebyshev polynomial
26
-/
0 commit comments