map_zero

Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

URI: https://scilib.ai/kg/mathlib#QuasispectrumRestricts.map_zero

English

The preimage of quasispectrum S a under algebraMap R S equals quasispectrum R a.

Русский

Обратноеобразование под отображением algebraMap R S от quasispectrum S a равно quasispectrum R a.

LaTeX

$$algebraMap R S ⁻¹' quasispectrum S a = quasispectrum R a$$

Lean4

protected theorem map_zero (h : QuasispectrumRestricts a f) : f 0 = 0 := by
  rw [← h.left_inv 0, map_zero (algebraMap R S)]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru