Theorems · Theorem · ring theory
RingHomCompTriple.comp_apply
∀ {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 σ₁₂ σ₂₃ σ₁₃] {x : R₁}, σ₂₃ (σ₁₂ x) = σ₁₃ x- Defined in
- Mathlib.Algebra.Ring.CompTypeclasses
- Cited by
- 42 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Semiringstatement and proof · cited by 13,802
- RingHomstatement and proof · cited by 10,189
- RingHomCompTriplestatement and proof · cited by 234
- RingHomCompTriple.comp_eqproof · cited by 38
- RingHom.congr_funproof · cited by 29
Cited by42
Results whose statement or proof uses this declaration.
- Module.Free.of_equivproof · cited by 23
- Module.Projective.of_equivproof · cited by 9
- Matrix.toLin_conjTransposeproof · cited by 4
- conjneg_conjnegproof · cited by 3
- UpperHalfPlane.σ_sqproof · cited by 2
- NumberField.ComplexEmbedding.isConj_apply_applyproof · cited by 2
- RingHom.RespectsIso.isLocalization_away_iffproof · cited by 2
- KaehlerDifferential.range_mapBaseChangeproof · cited by 2
- AlgebraicGeometry.exists_smooth_of_formallySmooth_stalkproof · cited by 2
- differentiableAt_star_conj_iffproof · cited by 2
- ArithmeticFunction.ofPowerSeries_apply_oneproof · cited by 2
- RingHom.OfLocalizationSpan.mkproof · cited by 1