Mathlib Changelog
Changelog
About
Github
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