Theorems · Theorem · ring theory

NonUnitalSubsemiring.comap_comap

∀ {R : Type u} {S : Type v} {T : Type w} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  [inst_2 : NonUnitalNonAssocSemiring T] {F : Type u_1} {G : Type u_2} [inst_3 : FunLike F R S]
  [inst_4 : NonUnitalRingHomClass F R S] [inst_5 : FunLike G S T] [inst_6 : NonUnitalRingHomClass G S T]
  (s : NonUnitalSubsemiring T) (g : G) (f : F),
  NonUnitalSubsemiring.comap f (NonUnitalSubsemiring.comap g s) = NonUnitalSubsemiring.comap ((↑g).comp ↑f) s

Defined in

Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonUnitalNonAssocSemiringNonUnitalNonAssocSemiringNonUnitalNonAssocSemiringFunLikeNonUnitalRingHomClassFunLikeNonUnitalRingHomClass