Theorems · Definition · nonassociative algebras

NonUnitalAlgHom.id

(R : Type u_2) →
  (A : Type u_3) →
    [inst : Monoid R] → [inst_1 : NonUnitalNonAssocSemiring A] → [inst_2 : DistribMulAction R A] → A →ₙₐ[R] A

The identity map as a NonUnitalAlgHom.

Defined in

Mathlib.Algebra.Algebra.NonUnitalHom

Cited by

5 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms

Assumes

MonoidNonUnitalNonAssocSemiringDistribMulAction