mk' — Mathlib

English

The map from AlgHom to RingHom is injective: if two AlgHoms have the same RingHom part, they are equal.

Русский

Отображение AlgHom в RingHom инъективно: одинаковая RingHom-часть двух AlgHom означает их равенство.

LaTeX

$$Function.Injective ((↑) : (A →ₐ[R] B) → A →+* B)$$

Lean4

/-- If a `RingHom` is `R`-linear, then it is an `AlgHom`. -/
def mk' (f : A →+* B) (h : ∀ (c : R) (x), f (c • x) = c • f x) : A →ₐ[R] B :=
  { f with
    toFun := f
    commutes' := fun c => by simp only [Algebra.algebraMap_eq_smul_one, h, f.map_one] }

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