aeval_derivative_mem_differentIdeal

English

A technical auxiliary result: from a maximal p in A and a P dividing the image of p in B, we obtain divisibility of a power minus one into the different ideal.

Русский

Техническое вспомогательное следствие: из максимального p в A и P делящего образ p в B следует делимость степени на разность в различном идеале.

LaTeX

$$P^{e-1} \;|\; \mathrm{differentIdeal}(A,B) \quad\text{under suitable hypotheses}$$

Lean4

theorem aeval_derivative_mem_differentIdeal (x : B) (hx : Algebra.adjoin K {algebraMap B L x} = ⊤) :
    aeval x (derivative (minpoly A x)) ∈ differentIdeal A B :=
  by
  refine SetLike.le_def.mp ?_ (Ideal.mem_span_singleton_self _)
  rw [← conductor_mul_differentIdeal A K L x hx]
  exact Ideal.mul_le_left

Похожие утверждения