mirror_mul_of_domain — Mathlib

English

The mirror operation distributes over multiplication: (p·q)̃ = p̃ · q̃ for polynomials p,q over a ring with no zero divisors.

Русский

Зеркалирование распределяется по умножению: (p q)̃ = p̃ q̃ при полиномах p, q над кольцом без нулевых делителей.

LaTeX

$$$ (p q)^{\\sim} = p^{\\sim} q^{\\sim} $$$

Lean4

theorem mirror_mul_of_domain : (p * q).mirror = p.mirror * q.mirror :=
  by
  by_cases hp : p = 0
  · rw [hp, zero_mul, mirror_zero, zero_mul]
  by_cases hq : q = 0
  · rw [hq, mul_zero, mirror_zero, mul_zero]
  rw [mirror, mirror, mirror, reverse_mul_of_domain, natTrailingDegree_mul hp hq, pow_add]
  rw [mul_assoc, ← mul_assoc q.reverse, ← X_pow_mul (p := reverse q)]
  repeat' rw [mul_assoc]

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