Theorems · Theorem · algebraic geometry

AlgebraicGeometry.StructureSheaf.const_mul_cancel

∀ {R : Type u} [inst : CommRing R] (f g₁ g₂ : R) (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (hu₁ : U ≤ PrimeSpectrum.basicOpen g₁) (hu₂ : U ≤ PrimeSpectrum.basicOpen g₂),
  AlgebraicGeometry.StructureSheaf.const f g₁ U hu₁ * AlgebraicGeometry.StructureSheaf.const g₁ g₂ U hu₂ =
    AlgebraicGeometry.StructureSheaf.const f g₂ U hu₂

Defined in: Mathlib.AlgebraicGeometry.StructureSheaf
Cited by: 1 results in Mathlib
Foundations: Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites15

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

CategoryTheory.Functor.objstatement and proof · cited by 19,642
CommRingstatement and proof · cited by 17,173
CategoryTheory.Functorstatement · cited by 16,252
Oppositestatement · cited by 8,081
TopCat.carrierstatement and proof · cited by 3,184
TopologicalSpace.Opensstatement and proof · cited by 2,040
CategoryTheory.ObjectProperty.FullSubcategory.objstatement and proof · cited by 1,316
CategoryTheory.Presheaf.IsSheafstatement · cited by 991
Opens.grothendieckTopologystatement · cited by 206
PrimeSpectrum.basicOpenstatement and proof · cited by 163
AlgebraicGeometry.PrimeSpectrum.Topstatement and proof · cited by 104
AlgebraicGeometry.structureSheafInTypestatement and proof · cited by 59

Cited by1

Results whose statement or proof uses this declaration.

AlgebraicGeometry.StructureSheaf.const_mul_cancel'proof · cited by 0