isQuasiregular_iff'

Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

URI: https://scilib.ai/kg/mathlib#isQuasiregular_iff'

← MathLib Explorer

English

IsQuasiregular x for x ∈ R is equivalent to IsUnit (PreQuasiregular.equiv x).

Русский

IsQuasiregular x эквивалентно IsUnit (PreQuasiregular.equiv x).

LaTeX

$$$$ IsQuasiregular(x) \iff IsUnit(PreQuasiregular.equiv(x)) $$$$

Lean4

theorem isQuasiregular_iff' {x : R} : IsQuasiregular x ↔ IsUnit (PreQuasiregular.equiv x) := by
  simp only [IsQuasiregular, IsUnit, Equiv.apply_symm_apply, ← PreQuasiregular.equiv (R := R).injective.eq_iff]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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