Theorems · Theorem · ring theory

Polynomial.coeff_opRingEquiv

∀ {R : Type u_1} [inst : Semiring R] (p : (Polynomial R)ᵐᵒᵖ) (n : ℕ),
  ((Polynomial.opRingEquiv R) p).coeff n = MulOpposite.op ((MulOpposite.unop p).coeff n)

Defined in

Mathlib.RingTheory.Polynomial.Opposites

Cited by

2 results in Mathlib

Foundations

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

Assumes

Semiring