toInvSubmonoid_surjective — Mathlib

English

The map toInvSubmonoid is surjective onto invSubmonoid, i.e., every inverted element comes from some m ∈ M.

Русский

Отображение toInvSubmonoid сюръективно по отношению к invSubmonoid: каждый инвертированный элемент имеется как образ некоторого m ∈ M.

LaTeX

$$$\text{toInvSubmonoid}: M \to_* \mathrm{invSubmonoid}(M,S)$ is surjective$$

Lean4

theorem toInvSubmonoid_surjective : Function.Surjective (toInvSubmonoid M S) :=
  Function.Surjective.comp (β := M.map (algebraMap R S)) (Equiv.surjective (equivInvSubmonoid _ _).toEquiv)
    (MonoidHom.submonoidMap_surjective _ _)

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