unitsFstOne — Mathlib

English

The subgroup of units of Unitization R A whose scalar part is 1 is isomorphic to the group of units of PreQuasiregular A.

Русский

Подгруппа единиц Unitization R A, чья скалярная часть равна 1, изоморфна группе единиц PreQuasiregular A.

LaTeX

$$$$ (unitsFstOne\ R\ A) \cong (PreQuasiregular\ A)^{\times} $$$$

Lean4

/-- The subgroup of the units of `Unitization R A` whose scalar part is `1`. -/
def unitsFstOne : Subgroup (Unitization R A)ˣ
    where
  carrier := {x | x.val.fst = 1}
  one_mem' := rfl
  mul_mem' {x} {y} (hx : fst x.val = 1) (hy : fst y.val = 1) := by simp [hx, hy]
  inv_mem' {x} (hx : fst x.val = 1) := by simpa [-Units.mul_inv, hx] using congr(fstHom R A $(x.mul_inv))

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