Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.PartialMap.comp_assoc

∀ {X₁ X₂ X₃ Y : AlgebraicGeometry.Scheme} [inst : PreirreducibleSpace ↥X₁] [inst_1 : IrreducibleSpace ↥X₂]
  [inst_2 : Nonempty ↥X₃] (f : X₁.PartialMap X₂) [inst_3 : AlgebraicGeometry.IsDominant f.hom] (g : X₂.PartialMap X₃)
  [inst_4 : AlgebraicGeometry.IsDominant g.hom] (h : X₃.PartialMap Y), (f.comp g).comp h = f.comp (g.comp h)

Defined in: Mathlib.AlgebraicGeometry.Birational.Composition
Cited by: 0 results in Mathlib
Foundations: Depth 153 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: PreirreducibleSpace IrreducibleSpace Nonempty AlgebraicGeometry.IsDominant AlgebraicGeometry.IsDominant

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites54

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

Quiver.Homproof · cited by 32,603
CategoryTheory.Functor.objproof · cited by 19,642
CategoryTheory.CategoryStruct.compproof · cited by 17,999
SetLike.coeproof · cited by 8,199
CategoryTheory.Iso.homproof · cited by 7,684
CategoryTheory.Iso.invproof · cited by 6,514
CategoryTheory.Category.assocproof · cited by 6,433
TopCat.carrierstatement and proof · cited by 3,184
LE.le.transproof · cited by 3,151
AlgebraicGeometry.Schemestatement and proof · cited by 2,540
CommRingCatstatement · cited by 2,333
Set.extproof · cited by 2,266

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.