leftInv — Mathlib

English

S.leftInv is the submonoid of M consisting of all left inverses of elements of S.

Русский

S.leftInv есть подмножество M, содержащее все левые обратные элементы элементов S.

LaTeX

$$S.leftInv is the submonoid with carrier { x ∈ M | ∃ y ∈ S, x y = 1 }.$$

Lean4

/-- `S.leftInv` is the submonoid containing all the left inverses of `S`. -/
@[to_additive /-- `S.leftNeg` is the additive submonoid containing all the left additive inverses of `S`. -/
    ]
def leftInv : Submonoid M where
  carrier := {x : M | ∃ y : S, x * y = 1}
  one_mem' := ⟨1, mul_one 1⟩
  mul_mem' := fun {a} _b ⟨a', ha⟩ ⟨b', hb⟩ ↦
    ⟨b' * a', by simp only [coe_mul, ← mul_assoc, mul_assoc a, hb, mul_one, ha]⟩

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