Theorems · Theorem · ring theory

RingHomSurjective.comp

∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomSurjective σ₁₂]
  [RingHomSurjective σ₂₃], RingHomSurjective σ₁₃

This cannot be an instance as there is no way to infer σ₁₂ and σ₂₃.

Defined in

Mathlib.Algebra.Ring.CompTypeclasses

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringSemiringSemiringRingHomCompTripleRingHomSurjectiveRingHomSurjective