English
Let R,S,T be domains with algebra structures and is integral on S, and f:R≃+*A, g:S≃+*T ring isomorphisms that compatibly relate the structure maps (the compatiblity condition is given). Then map f applied to minpoly_R x equals minpoly_A applied to g x.
Русский
Пусть R,S,T — области с алгебраическими структурами, существуют совместимые изоморфизмы колец f и g, и тогда отображение minpoly через f переносится на minpoly через g.
LaTeX
$$map f (minpoly R x) = minpoly A (g x)$$
Lean4
/-- The constant coefficient of the minimal polynomial of `x` is `0` if and only if `x = 0`. -/
@[simp]
theorem coeff_zero_eq_zero (hx : IsIntegral A x) : coeff (minpoly A x) 0 = 0 ↔ x = 0 :=
by
constructor
· intro h
have zero_root := zero_isRoot_of_coeff_zero_eq_zero h
rw [← root hx zero_root]
exact RingHom.map_zero _
· rintro rfl
simp
