isQuasiregular_inr_iff — Mathlib

English

For a ∈ A, IsQuasiregular (a in unitization R A) holds if and only if IsQuasiregular a holds.

Русский

Для элемента a ∈ A выполняется: IsQuasiregular (a в единичной декомпозиции Unitization) тогда и только тогда, когда IsQuasiregular a.

LaTeX

$$IsQuasiregular (a : Unitization R A) \iff IsQuasiregular a$$

Lean4

theorem isQuasiregular_inr_iff (a : A) : IsQuasiregular (a : Unitization R A) ↔ IsQuasiregular a :=
  by
  refine ⟨fun ha ↦ ?_, IsQuasiregular.map (inrNonUnitalAlgHom R A)⟩
  rw [isQuasiregular_iff] at ha ⊢
  obtain ⟨y, hy₁, hy₂⟩ := ha
  lift y to A using by simpa using congr(fstHom R A $(hy₁))
  refine ⟨y, ?_, ?_⟩ <;> exact inr_injective (R := R) <| by simpa

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