mul_comm_iff — Mathlib

English

For f: S → R and a,b ∈ A, QuasispectrumRestricts (a·b) f is equivalent to QuasispectrumRestricts (b·a) f.

Русский

Для отображения f: S → R и элементов a, b ∈ A, ограничение квазиспеktrа на a·b эквивалентно ограничению на b·a.

LaTeX

$$$\\mathrm{QuasispectrumRestricts}(a b,f) \\iff \\mathrm{QuasispectrumRestricts}(b a,f)$$$

Lean4

theorem mul_comm_iff {f : S → R} {a b : A} : QuasispectrumRestricts (a * b) f ↔ QuasispectrumRestricts (b * a) f := by
  simp only [quasispectrumRestricts_iff, quasispectrum.mul_comm]

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