Psi injective

theorem psi_injective (α k : ℕ) (h2 : (2 : R) ≠ 0) (hk2pow : ∃ κ, k = 2 ^ κ)    (hk : 2 * k ∣ 2 ^ α) : Function.Injective (psi (R := R) α k) := by  obtain ⟨κ, rfl⟩ := hk2pow  have hκ : κ ≤ α := Nat.le_of_succ_le (succ_le_of_two_mul_two_pow_dvd hk)  have hunit : IsUnit ((2 ^ α / 2 ^ κ : ℕ) : Rq (powTwoCyclotomic (R := R) α)) := by    rw [Nat.pow_div hκ (by norm_num), Nat.cast_pow, Nat.cast_ofNat]    exact (isUnit_two (powTwoCyclotomic α) h2).pow _  intro a b hab  funext j  have ha := traceH_psi_mul_conj α (2 ^ κ) h2 ⟨κ, rfl⟩ hk a (Pi.single j 1)  have hb := traceH_psi_mul_conj α (2 ^ κ) h2 ⟨κ, rfl⟩ hk b (Pi.single j 1)  rw [hab] at ha  have heq := ha.symm.trans hb  rw [nsmul_eq_mul, nsmul_eq_mul] at heq  have hcancel := hunit.mul_left_cancel heq  simp only [Pi.single_apply, mul_ite, mul_one, mul_zero, Finset.sum_ite_eq', Finset.mem_univ,    if_true] at hcancel  exact Subtype.coe_injective hcancel