Theorems · Theorem · nonassociative algebras

NonUnitalAlgHom.comp.congr_simp

∀ {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 f_1 : B →ₛₙₐ[ψ] C),
  f = f_1 → ∀ (g g_1 : A →ₛₙₐ[φ] B), g = g_1 → ∀ [κ : φ.CompTriple ψ χ], f.comp g = f_1.comp g_1

Defined in

Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Cited by

0 results in Mathlib

Foundations

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

Assumes

MonoidMonoidMonoidNonUnitalNonAssocSemiringDistribMulActionNonUnitalNonAssocSemiringDistribMulActionNonUnitalNonAssocSemiringDistribMulActionMonoidHom.CompTriple