Mathlib v3 is deprecated. Go to Mathlib v4

Theorem algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.mem_carrier_iff'

Modification history

2022-10-05 18:04
src/algebraic_geometry/projective_spectrum/scheme.lean
refactor(algebraic_geometry/projective_spectrum/scheme): use homogenous localization API (#16693)
Added algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.mem_carrier_iff'View on Github →