Theorems · Theorem · commutative algebra

Subsemiring.map_map

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

Defined in

Mathlib.Algebra.Ring.Subsemiring.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

NonAssocSemiringNonAssocSemiringNonAssocSemiring