algEquiv_eq

Mathlib.FieldTheory.Minpoly.Basic

URI: https://scilib.ai/kg/mathlib#minpoly.algEquiv_eq

English

If f is an algebra isomorphism A B B', then minpoly_A(f(x)) = minpoly_A(x).

Русский

Если f — алгебра-изоморфизм A B B', то минимальный многочлен сохраняется: minpoly_A(f(x)) = minpoly_A(x).

LaTeX

$$$\\minpoly_{A}(f(x)) = \\minpoly_{A}(x).$$$

Lean4

@[simp]
theorem algEquiv_eq (f : B ≃ₐ[A] B') (x : B) : minpoly A (f x) = minpoly A x :=
  algHom_eq (f : B →ₐ[A] B') f.injective x

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru