Zulip Chat Archive
Stream: lean4
Topic: The data type changed
SHAO YU (Jul 22 2024 at 05:13):
lemma explore_01 (n k m l:ℕ )(x: ℝ )(h₁: m ≤ n)(h₂: k ≤ m)(h₃:m=2*l)(h₄: k ≤ n):
((1+x)^n)*((1-x)^n)= ∑ m in range (2*n+1),(∑ k in range (m+1),(n.choose k)* n.choose (m-k) * ((-1):ℝ )^ k )* x^m := by
have _01 (x : ℝ ) : ( 1 + x ) ^ n = ∑ k in range ( n + 1 ),( n.choose k )* x ^ k := by
rw [cast_id n]
rw [add_comm,add_pow]
rw [Finset.sum_congr];simp
intro k hk
simp;
rw[mul_comm]
The data type of n changed from N to R, causing some strategies to use cast_id, but reported wrong, what should I do?
Last updated: May 02 2025 at 03:31 UTC