Theorems · Theorem · ring theory

Polynomial.opRingEquiv_op_monomial

∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (r : R),
  (Polynomial.opRingEquiv R) (MulOpposite.op ((Polynomial.monomial n) r)) = (Polynomial.monomial n) (MulOpposite.op r)

Defined in

Mathlib.RingTheory.Polynomial.Opposites

Cited by

3 results in Mathlib

Foundations

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

Assumes

Semiring