mrange_mk' — Mathlib

English

The image of the kernel lift along a monoid homomorphism f equals the image of f itself: mrange (kerLift f) = mrange f.

Русский

Образ подъёма ядра вдоль гомоморфизма f равен образу самого f: mrange (kerLift f) = mrange f.

LaTeX

$$MonoidHom.mrange (kerLift f) = MonoidHom.mrange f$$

Lean4

@[to_additive (attr := simp)]
  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11036): removed dot notation

theorem mrange_mk' : MonoidHom.mrange c.mk' = ⊤ :=
  MonoidHom.mrange_eq_top.2 mk'_surjective

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