Mathlib v3 is deprecated. Go to Mathlib v4

Theorem algebraic_geometry.structure_sheaf.to_pushforward_stalk_comp

Modification history

2022-12-07 08:32

src/algebraic_geometry/Spec.lean

feat(algebraic_geometry/Spec): `(f∗ 𝒪ₛ)ₚ` is just the localization `Sₚ` for affine `f : Spec S ⟶ Spec R` (#17471)

Added algebraic_geometry.structure_sheaf.to_pushforward_stalk_comp View on Github →