preimage_units_mul_comm — Mathlib

English

Let a,b ∈ A be elements and consider their spectra in R via Units.val. Then the preimage of σ(a·b) under Units.val equals the preimage of σ(b·a).

Русский

Пусть a,b ∈ A и рассматриваются их спектры через отображение Units.val. Тогда предобраз σ(a·b) и σ(b·a) совпадают.

LaTeX

$$$((\uparrow) : R^{\times} \to R)^{-1}'\sigma(a b) = (\uparrow)^{-1}'\sigma(b a)$$$

Lean4

theorem preimage_units_mul_comm (a b : A) : ((↑) : Rˣ → R) ⁻¹' σ (a * b) = (↑) ⁻¹' σ (b * a) :=
  Set.ext fun _ => unit_mem_mul_comm

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