unitGroupMulEquiv — Mathlib

English

There is a multiplicative equivalence between the unit group of A and the group of units of A, i.e., A.unitGroup ≃* Aˣ.

Русский

Существует переходом по умножению биективное соответствие между группой единиц A и группой единиц A; то есть A.unitGroup ≃* Aˣ.

LaTeX

$$$A_{\mathrm{unitGroup}} \cong_{\ast} A^{\times}$$$

Lean4

/-- For a valuation subring `A`, `A.unitGroup` agrees with the units of `A`. -/
def unitGroupMulEquiv : A.unitGroup ≃* Aˣ
    where
  toFun
    x :=
    { val := ⟨(x : Kˣ), mem_of_valuation_le_one A _ x.prop.le⟩
      inv := ⟨((x⁻¹ : A.unitGroup) : Kˣ), mem_of_valuation_le_one _ _ x⁻¹.prop.le⟩
      val_inv := Subtype.ext (by simp)
      inv_val := Subtype.ext (by simp) }
  invFun x := ⟨Units.map A.subtype.toMonoidHom x, A.valuation_unit x⟩
  map_mul' a b := by ext; rfl

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