instInvValueGroup — Mathlib

English

Inverse on ValueGroup(A,K) is induced by inverses of representatives: (a)^{-1} is class of a^{-1}.

Русский

Обратный элемент в ValueGroup(A,K) индуцирован через обратное к представителю: A^{-1}.

LaTeX

$$$\mathrm{Inv}(\mathrm{ValueGroup}(A,K))$ is defined by $\mathrm{Quotient}.lift'\, a \mapsto \mathrm{Quotient}.mk'' a^{-1}$.$$

Lean4

instance : Inv (ValueGroup A K) :=
  Inv.mk fun x =>
    Quotient.liftOn' x (fun a => Quotient.mk'' a⁻¹)
      (by
        rintro _ a ⟨b, rfl⟩
        apply Quotient.sound'
        use b⁻¹
        dsimp
        rw [Units.smul_def, Units.smul_def, Algebra.smul_def, Algebra.smul_def, mul_inv, map_units_inv])

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