Theorems · Theorem · field theory

Polynomial.leadingCoeff_map

∀ {R : Type u} {S : Type v} [inst : Ring R] [IsSimpleRing R] [inst_2 : Semiring S] [Nontrivial S] {p : Polynomial R}
  (f : R →+* S), (Polynomial.map f p).leadingCoeff = f p.leadingCoeff

Defined in

Mathlib.Algebra.Polynomial.FieldDivision

Cited by

11 results in Mathlib

Foundations

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

Assumes

RingIsSimpleRingSemiringNontrivial