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.is_localized_module_to_pushforward_stalk_alg_hom_aux