leftInv_eq_inv — Mathlib

English

In a group, the leftInv submonoid equals the inverse submonoid: S.leftInv = S^{-1}.

Русский

В группе подмножество левых обратных совпадает с подмножеством обратных: S.leftInv = S^{-1}.

LaTeX

$$$ S.leftInv = S^{-1} $$$

Lean4

@[to_additive]
theorem leftInv_eq_inv : S.leftInv = S⁻¹ :=
  Submonoid.ext fun _ ↦
    ⟨fun h ↦ Submonoid.mem_inv.mpr ((inv_eq_of_mul_eq_one_right h.choose_spec).symm ▸ h.choose.prop), fun h ↦
      ⟨⟨_, h⟩, mul_inv_cancel _⟩⟩

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