Theorems · Theorem · commutative algebra

Subsemiring.comap_comap

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

Defined in: Mathlib.Algebra.Ring.Subsemiring.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 20 from the axioms · uses propext, Quot.sound
Assumes: NonAssocSemiring NonAssocSemiring NonAssocSemiring

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

RingHomstatement and proof · cited by 10,189
RingHom.compstatement · cited by 899
NonAssocSemiringstatement and proof · cited by 805
Subsemiringstatement and proof · cited by 456
Subsemiring.comapstatement · cited by 20

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.