Theorems · Theorem · field theory

minpoly.algebraMap_eq

∀ {A : Type u_1} {B' : Type u_3} [inst : CommRing A] [inst_1 : Ring B'] [inst_2 : Algebra A B'] {B : Type u_4}
  [inst_3 : CommRing B] [inst_4 : Algebra A B] [inst_5 : Algebra B B'] [IsScalarTower A B B'],
  Function.Injective ⇑(algebraMap B B') → ∀ (x : B), minpoly A ((algebraMap B B') x) = minpoly A x

Defined in

Mathlib.FieldTheory.Minpoly.Basic

Cited by

9 results in Mathlib

Foundations

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

Assumes

CommRingRingAlgebraCommRingAlgebraAlgebraIsScalarTower