inv_mem_of_root_of_coeff_zero_ne_zero

English

If aeval x p = 0 and p.coeff 0 ≠ 0 then x⁻¹ belongs to the ambient algebra, expressed via Aeval and algebra maps.

Русский

Если aeval x p = 0 и p(0) ≠ 0, то x⁻¹ принадлежит окружению алгебры, выражено через aeval и алгебраическое отображение.

LaTeX

$$$(x^{-1} \\in L)$ очевидно из условий; записывается как \$x^{-1} \\in A\$ в контексте подалгебры.$$

Lean4

theorem inv_mem_of_root_of_coeff_zero_ne_zero {x : A} {p : K[X]} (aeval_eq : aeval x p = 0)
    (coeff_zero_ne : p.coeff 0 ≠ 0) : (x⁻¹ : L) ∈ A :=
  by
  suffices (x⁻¹ : L) = (-p.coeff 0)⁻¹ • aeval x (divX p)
    by
    rw [this]
    exact A.smul_mem (aeval x _).2 _
  have : aeval (x : L) p = 0 := by rw [Subalgebra.aeval_coe, aeval_eq, Subalgebra.coe_zero]
  rw [inv_eq_of_root_of_coeff_zero_ne_zero this coeff_zero_ne, div_eq_inv_mul, Algebra.smul_def, aeval_coe, map_inv₀,
    map_neg, inv_neg, neg_mul]

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