English
Let R be a semiring and f,g ∈ R[X] with natDegree f ≤ F and natDegree g ≤ G. Then the F+G-reverse of the product f g equals the product of the F-reverse of f and the G-reverse of g.
Русский
Пусть R — полукольцо, и f,g ∈ R[X] такие, что natDegree f ≤ F и natDegree g ≤ G. Тогда отражение (F+G) от произведения f g равно произведению отражений: reflect F f и reflect G g.
LaTeX
$$$\operatorname{reflect}(F+G)(f g) = \operatorname{reflect} F f \cdot \operatorname{reflect} G g, \quad \text{при } \operatorname{natDegree}(f) \le F, \operatorname{natDegree}(g) \le G.$$$
Lean4
@[simp]
theorem reflect_mul (f g : R[X]) {F G : ℕ} (Ff : f.natDegree ≤ F) (Gg : g.natDegree ≤ G) :
reflect (F + G) (f * g) = reflect F f * reflect G g :=
reflect_mul_induction _ _ F G f g f.support.card.le_succ g.support.card.le_succ Ff Gg
