mirror_smul — Mathlib

English

Over rings with no zero divisors, mirror respects multiplication: mirror(p q) = mirror(p) mirror(q).

Русский

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

LaTeX

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

Lean4

theorem mirror_smul (a : R) : (a • p).mirror = a • p.mirror := by
  rw [← C_mul', ← C_mul', mirror_mul_of_domain, mirror_C]

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