Theorems · Definition · ring theory

AlgEquiv.toAlgHom

{R : Type uR} →
  {A₁ : Type uA₁} →
    {A₂ : Type uA₂} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A₁] →
          [inst_2 : Semiring A₂] → [inst_3 : Algebra R A₁] → [inst_4 : Algebra R A₂] → (A₁ ≃ₐ[R] A₂) → A₁ →ₐ[R] A₂

Interpret an algebra equivalence as an algebra homomorphism. This definition is included for symmetry with the other to*Hom projections. The simp normal form is to use the coercion of the AlgHomClass.coeTC instance.

Defined in

Mathlib.Algebra.Algebra.Equiv

Cited by

273 results in Mathlib

Foundations

Depth 23 from the axioms, rests on 175 definitions · uses propext, Quot.sound

Assumes

CommSemiringSemiringSemiringAlgebraAlgebra