inv_mem_iff — Mathlib

English

Let r ∈ Units R and a ∈ Units A. If r ∈ resolventSet(R,a) for a, then r⁻¹ ∈ resolventSet(R, a⁻¹).

Русский

Пусть r ∈ единицы R и a ∈ единицы A. Если r ∈ резольвентное множество( R, a ), то r⁻¹ ∈ резольвентное множество( R, a⁻¹ ).

LaTeX

$$$\text{If } r \in R^{\times} \text{ and } a \in A^{\times}, \ r \in \operatorname{resolventSet}(R,a) \Rightarrow r^{-1} \in \operatorname{resolventSet}(R, a^{-1})$$$

Lean4

theorem inv_mem_iff {r : Rˣ} {a : Aˣ} : (r : R) ∈ σ (a : A) ↔ (↑r⁻¹ : R) ∈ σ (↑a⁻¹ : A) :=
  not_iff_not.2 <| ⟨inv_mem_resolventSet, inv_mem_resolventSet⟩

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