reverse_mul_of_domain — Mathlib

English

Over a domain (NoZeroDivisors), reverse(f g) = reverse(f) · reverse(g) for all polynomials f,g.

Русский

В области (без делителей нуля) для любых многочленов f,g выполняется reverse(f g) = reverse(f) · reverse(g).

LaTeX

$$$\text{If } R \text{ is a semiring with no zero divisors, then } \operatorname{reverse}(f g) = \operatorname{reverse}(f) \operatorname{reverse}(g).$$$

Lean4

@[simp]
theorem reverse_mul_of_domain {R : Type*} [Semiring R] [NoZeroDivisors R] (f g : R[X]) :
    reverse (f * g) = reverse f * reverse g := by
  by_cases f0 : f = 0
  · simp only [f0, zero_mul, reverse_zero]
  by_cases g0 : g = 0
  · rw [g0, mul_zero, reverse_zero, mul_zero]
  simp [reverse_mul, *]

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