mul_comm_iff — Mathlib

English

SpectrumRestricts is invariant under swapping the factors in a product: SpectrumRestricts (a·b) f ↔ SpectrumRestricts (b·a) f.

Русский

Свойство SpectrumRestricts сохраняется при перестановке множителей в произведении: SpectrumRestricts (a·b) f ↔ SpectrumRestricts (b·a) f.

LaTeX

$$$ SpectrumRestricts (a \\cdot b)\\ f \\iff SpectrumRestricts (b \\cdot a)\\ f $$$

Lean4

theorem mul_comm_iff {R S A : Type*} [Semifield R] [Field S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A]
    {a b : A} {f : S → R} : SpectrumRestricts (a * b) f ↔ SpectrumRestricts (b * a) f :=
  QuasispectrumRestricts.mul_comm_iff

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