Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-01 11:59 23b01cc4

View on Github →

feat(algebraic_geometry): The function field of an integral scheme (#11147)

Estimated changes

Modified src/algebra/field/basic.lean

Created src/algebraic_geometry/function_field.lean

added def algebraic_geometry.Scheme.function_field

added def algebraic_geometry.Scheme.germ_to_function_field

added theorem algebraic_geometry.Scheme.germ_to_function_field_injective

added theorem algebraic_geometry.germ_injective_of_is_integral

Modified src/algebraic_geometry/prime_spectrum/basic.lean

Modified src/algebraic_geometry/properties.lean

added theorem algebraic_geometry.affine_is_integral_iff

added theorem algebraic_geometry.affine_is_reduced_iff

added theorem algebraic_geometry.is_integral_iff_is_irreducible_and_is_reduced

added theorem algebraic_geometry.is_integral_of_is_irreducible_is_reduced

added theorem algebraic_geometry.is_integral_of_open_immersion

added theorem algebraic_geometry.map_injective_of_is_integral

Modified src/topology/opens.lean

added theorem topological_space.opens.coe_top

added theorem topological_space.opens.ne_bot_iff_nonempty

added theorem topological_space.opens.not_nonempty_iff_eq_bot