Commit 2023-06-30 18:41 e3884c33

View on Github →

feat: port AlgebraicGeometry.FunctionField (#5596)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/FunctionField.lean

added theorem AlgebraicGeometry.IsAffineOpen.primeIdealOf_genericPoint

added theorem AlgebraicGeometry.Scheme.germToFunctionField_injective

added theorem AlgebraicGeometry.functionField_isFractionRing_of_isAffineOpen

added theorem AlgebraicGeometry.genericPoint_eq_bot_of_affine

added theorem AlgebraicGeometry.genericPoint_eq_of_isOpenImmersion

added theorem AlgebraicGeometry.germ_injective_of_isIntegral

Modified Mathlib/AlgebraicGeometry/Scheme.lean

added theorem AlgebraicGeometry.Scheme.comp_val_base_apply