Theorems · Theorem · field theory

Polynomial.Splits.of_algHom

∀ {R : Type u_1} [inst : CommSemiring R] {f : Polynomial R} {A : Type u_2} {B : Type u_3} [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B],
  (Polynomial.map (algebraMap R A) f).Splits → ∀ (e : A →ₐ[R] B), (Polynomial.map (algebraMap R B) f).Splits

Defined in

Mathlib.Algebra.Polynomial.Splits

Cited by

3 results in Mathlib

Foundations

Depth 108 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringSemiringSemiringAlgebraAlgebra