preimage_algebraMap — Mathlib

English

If h is a QuasispectrumRestricts a f and s ∈ quasispectrum S a, then f s ∈ quasispectrum R a.

Русский

Если h — это QuasispectrumRestricts a f и s ∈ quasispectrum S a, то f s ∈ quasispectrum R a.

LaTeX

$$QuasispectrumRestricts a f → ∀ {s}, s ∈ quasispectrum S a → f s ∈ quasispectrum R a$$

Lean4

@[simp]
theorem preimage_algebraMap (S : Type*) {R A : Type*} [Semifield R] [Field S] [NonUnitalRing A] [Algebra R S]
    [Module S A] [IsScalarTower S A A] [SMulCommClass S A A] [Module R A] [IsScalarTower R S A] {a : A} :
    algebraMap R S ⁻¹' quasispectrum S a = quasispectrum R a :=
  Set.ext fun _ => quasispectrum.algebraMap_mem_iff _

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