Theorems · Theorem · nonassociative algebras

NonUnitalAlgHom.coe_comp

∀ {R : Type u} {S : Type u₁} {T : Type u_1} [inst : Monoid R] [inst_1 : Monoid S] [inst_2 : Monoid T] {φ : R →* S}
  {A : Type v} {B : Type w} {C : Type w₁} [inst_3 : NonUnitalNonAssocSemiring A] [inst_4 : DistribMulAction R A]
  [inst_5 : NonUnitalNonAssocSemiring B] [inst_6 : DistribMulAction S B] [inst_7 : NonUnitalNonAssocSemiring C]
  [inst_8 : DistribMulAction T C] {ψ : S →* T} {χ : R →* T} (f : B →ₛₙₐ[ψ] C) (g : A →ₛₙₐ[φ] B)
  [inst_9 : φ.CompTriple ψ χ], ⇑(f.comp g) = ⇑f ∘ ⇑g

Defined in

Mathlib.Algebra.Algebra.NonUnitalHom

Cited by

0 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext, Quot.sound

Assumes

MonoidMonoidMonoidNonUnitalNonAssocSemiringDistribMulActionNonUnitalNonAssocSemiringDistribMulActionNonUnitalNonAssocSemiringDistribMulActionMonoidHom.CompTriple