Mathlib v3 is deprecated. Go to Mathlib v4

Def algebraic_geometry.structure_sheaf.to_pushforward_stalk_alg_hom

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_alg_hom View on Github →