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