∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  (F : Polynomial R) (a : ℤ_[p]),
  T_gen✝ p F a = ‖↑((Polynomial.aeval a) F) / ↑((Polynomial.aeval a) (Polynomial.derivative F) ^ 2)‖