kerLift_range_eq — Mathlib

English

In the same setting, the image of the kerLift f map equals the image of f.

Русский

В той же постановке образ kerLift f совпадает с образом f.

LaTeX

$$$\operatorname{mrange}(\kerLift f) = \operatorname{mrange}(f)$$$

Lean4

/-- Given a monoid homomorphism `f`, the induced homomorphism on the quotient by `f`'s kernel has
the same image as `f`. -/
@[to_additive (attr := simp) /-- Given an `AddMonoid` homomorphism `f`, the induced homomorphism
    on the quotient by `f`'s kernel has the same image as `f`. -/
    ]
theorem kerLift_range_eq : MonoidHom.mrange (kerLift f) = MonoidHom.mrange f :=
  lift_range fun _ _ => id

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