Theorems · Theorem · ring theory

TrivSqZeroExt.map_comp_map

∀ {R' : Type u} {M : Type v} [inst : CommSemiring R'] [inst_1 : AddCommMonoid M] [inst_2 : Module R' M]
  [inst_3 : Module R'ᵐᵒᵖ M] [inst_4 : IsCentralScalar R' M] {N : Type u_3} {P : Type u_4} [inst_5 : AddCommMonoid N]
  [inst_6 : Module R' N] [inst_7 : Module R'ᵐᵒᵖ N] [inst_8 : IsCentralScalar R' N] [inst_9 : AddCommMonoid P]
  [inst_10 : Module R' P] [inst_11 : Module R'ᵐᵒᵖ P] [inst_12 : IsCentralScalar R' P] (f : M →ₗ[R'] N) (g : N →ₗ[R'] P),
  TrivSqZeroExt.map (g ∘ₗ f) = (TrivSqZeroExt.map g).comp (TrivSqZeroExt.map f)

Defined in

Mathlib.Algebra.TrivSqZeroExt.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleModuleIsCentralScalarAddCommMonoidModuleModuleIsCentralScalarAddCommMonoidModuleModuleIsCentralScalar