Polynomial.opRingEquiv_symm_monomial
theorem 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) r.unop)
The theorem `Polynomial.opRingEquiv_symm_monomial` states that for any semiring `R`, natural number `n` and an element `r` of the opposite ring of `R`, the inverse of the ring isomorphism (`RingEquiv.symm`) transformed by `Polynomial.opRingEquiv R` and applied to the monomial `n` of `r` (`Polynomial.monomial n r`) is equivalent to the monomial `n` applied to the unopposite of `r` (`MulOpposite.unop r`) and then made opposite (`MulOpposite.op`). In other words, switching the roles of addition and multiplication in a polynomial ring `R` and then taking a monomial doesn't change the monomial if you switch the roles of addition and multiplication back in the coefficients.
More concisely: For any semiring `R`, the application of `Polynomial.opRingEquiv R` to the monomial `n` of an element `r` in the opposite ring of `R` is equivalent to the monomial `n` applied to the unopposite of `r` and made opposite.
|
Polynomial.opRingEquiv_op_monomial
theorem 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)
The theorem `Polynomial.opRingEquiv_op_monomial` states for any semiring `R`, natural number `n` and element `r` of `R`, applying the ring isomorphism `Polynomial.opRingEquiv R` to the element obtained by applying the `MulOpposite.op` operation to the monomial `a * X^n` where `a` is `r`, is the same as applying the `MulOpposite.op` operation to `r` and then creating the corresponding monomial. In simpler terms, it says that changing the order of operations — creating a monomial first then taking the opposite, or taking the opposite first then creating a monomial — doesn't change the final result.
More concisely: For any semiring `R`, applying the ring isomorphism `Polynomial.opRingEquiv R` to the monomial obtained by applying `MulOpposite.op` to `r * X^n` is equivalent to applying `MulOpposite.op` to `r` and then creating the monomial `X^n`.
|