chore(field_theory/laurent): drop unused 'have'. (#12516)

leanprover-community · Mar 8, 2022 · b4a7ad6 · b4a7ad6
1 parent dc093e9
commit b4a7ad6
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/src/field_theory/laurent.lean b/src/field_theory/laurent.lean
@@ -38,7 +38,6 @@ begin
   intros x hx,
   have : x = taylor (r - r) x,
   { simp },
-  have ht := polynomial.taylor_injective r,
   rwa [this, sub_eq_add_neg, ←taylor_taylor, ←taylor_mul,
        linear_map.map_eq_zero_iff _ (taylor_injective _),
        mul_right_mem_non_zero_divisors_eq_zero_iff hp,