ofInjective_toHom — Mathlib

English

In an algebraic language, if f: M →[L] N is injective, then the embedding constructed from f has toHom equal to f.

Русский

В алгебраическом языке, если f: M →[L] N инъективно, то вложение, построенное из f, имеет toHom равный f.

LaTeX

$$$(\\mathrm{ofInjective}\\ hf).toHom = f$$$

Lean4

@[simp]
theorem ofInjective_toHom [L.IsAlgebraic] {f : M →[L] N} (hf : Function.Injective f) : (ofInjective hf).toHom = f := by
  ext; simp

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