Theorems · Theorem · ring theory

Polynomial.opRingEquiv_symm_monomial

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

Defined in

Mathlib.RingTheory.Polynomial.Opposites

Cited by

3 results in Mathlib

Foundations

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

Assumes

Semiring