isUnit_one_add — Mathlib

English

For x in A (where A is a non-unital algebra over a commutative ring), IsQuasiregular x is equivalent to IsUnit (1 + x) in the Unitization R A.

Русский

Для x в A, IsQuasiregular x эквивалентно IsUnit (1+x) в Unitization R A.

LaTeX

$$$$ IsQuasiregular(x) \iff IsUnit(1+x \text{ in Unitization } R A) $$$$

Lean4

theorem isUnit_one_add {R : Type*} [Semiring R] {x : R} (hx : IsQuasiregular x) : IsUnit (1 + x) :=
  by
  obtain ⟨y, hy₁, hy₂⟩ := isQuasiregular_iff.mp hx
  refine ⟨⟨1 + x, 1 + y, ?_, ?_⟩, rfl⟩
  · convert congr(1 + $(hy₁)) using 1 <;> [noncomm_ring; simp]
  · convert congr(1 + $(hy₂)) using 1 <;> [noncomm_ring; simp]

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