Theorems · Theorem · ring theory

NonUnitalSubring.map_map

∀ {R : Type u} {S : Type v} {T : Type u_1} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
  [inst_2 : NonUnitalNonAssocRing T] (s : NonUnitalSubring R) (g : S →ₙ+* T) (f : R →ₙ+* S),
  NonUnitalSubring.map g (NonUnitalSubring.map f s) = NonUnitalSubring.map (g.comp f) s

Defined in

Mathlib.RingTheory.NonUnitalSubring.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

NonUnitalNonAssocRingNonUnitalNonAssocRingNonUnitalNonAssocRing