quotKerEquivOfSurjective_apply_mk

English

For surjective f, the isomorphism applied to the quotient class of x equals f(x).

Русский

Для сюръективного f изоморфизм на класс x в произведении равен f(x).

LaTeX

$$(f.quotKerEquivOfSurjective hf (Submodule.Quotient.mk x) : M₂) = f x$$

Lean4

@[simp]
theorem quotKerEquivOfSurjective_apply_mk (hf : Function.Surjective f) (x : M) :
    (f.quotKerEquivOfSurjective hf (Submodule.Quotient.mk x) : M₂) = f x :=
  rfl

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