Theorems · Inductive type · ring theory

RingHomCompTriple

{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₃) → outParam (R₁ →+* R₃) → Prop

Class that expresses the fact that three ring homomorphisms form a composition triple. This is used to handle composition of semilinear maps.

Defined in

Mathlib.Algebra.Ring.CompTypeclasses

Cited by

234 results in Mathlib

Foundations

Depth 11 from the axioms, rests on 81 definitions · uses no axioms

Assumes

SemiringSemiringSemiring