Theorems · Theorem · nonassociative algebras

NonUnitalAlgHom.snd_toFun

∀ (R : Type u) [inst : Monoid R] (A : Type v) (B : Type w) [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : DistribMulAction R B] (self : A × B),
  (NonUnitalAlgHom.snd R A B) self = self.2

Defined in

Mathlib.Algebra.Algebra.NonUnitalHom

Cited by

0 results in Mathlib

Foundations

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

Assumes

MonoidNonUnitalNonAssocSemiringDistribMulActionNonUnitalNonAssocSemiringDistribMulAction