toAlgHom_ofBijective — Mathlib

English

The algebra hom embedded in the promoted equivalence equals the original f, i.e., AlgHomClass.toAlgHom (ofBijective f hf) = f.

Русский

Алгебра-гомоморфизм, сопоставляемый продвинутой эквивалентности, равен исходному f: AlgHomClass.toAlgHom (ofBijective f hf) = f.

LaTeX

$$$\\mathrm{AlgHomClass.toAlgHom}(\\mathrm{ofBijective}(f, hf)) = f$$$

Lean4

@[simp]
theorem toAlgHom_ofBijective (f : A₁ →ₐ[R] A₂) (hf : Function.Bijective f) :
    AlgHomClass.toAlgHom (ofBijective f hf) = f :=
  rfl

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