opRingEquiv_op_C_mul_X_pow — Mathlib

English

For any r ∈ R and n ∈ N, opRingEquiv(op(C r) * X^n) = C(op r) * X^n.

Русский

Для любого r ∈ R и натурального n выполняется опобразование: op(C r) * X^n подействовало образуется C(op r) * X^n.

LaTeX

$$$\operatorname{opRingEquiv}(R)(\operatorname{op}(C r) \cdot X^{n}) = C(\operatorname{op} r) \cdot X^{n}$$$

Lean4

theorem opRingEquiv_op_C_mul_X_pow (r : R) (n : ℕ) : opRingEquiv R (op (C r * X ^ n : R[X])) = C (op r) * X ^ n := by
  simp only [X_pow_mul, op_mul, op_pow, map_mul, map_pow, opRingEquiv_op_X, opRingEquiv_op_C]

Похожие утверждения