isConjRoot_of_algEquiv'

Mathlib.FieldTheory.Minpoly.IsConjRoot

URI: https://scilib.ai/kg/mathlib#isConjRoot_of_algEquiv'

← MathLib Explorer

English

Variant: isConjRoot_of_algEquiv' asserts IsConjRoot R (s x) x.

Русский

Вариант: isConjRoot_of_algEquiv' утверждает IsConjRoot R (s x) x.

LaTeX

$$IsConjRoot R (s x) x$$

Lean4

/-- A variant of `isConjRoot_of_algEquiv`.
Let `s` be an `R`-algebra isomorphism. Then `x` is a conjugate root of `s x`.
-/
@[simp]
theorem isConjRoot_of_algEquiv' (x : A) (s : A ≃ₐ[R] A) : IsConjRoot R (s x) x :=
  (minpoly.algEquiv_eq s x)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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