Theorem AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality

Modification history

2024-10-16 11:05
Mathlib/Geometry/RingedSpace/LocallyRingedSpace/ResidueField.lean
refactor(AlgebraicGeometry): Make `Scheme.Hom` a structure. (#15093) …
Modified AlgebraicGeometry.LocallyRingedSpace.evaluation_naturalityView on Github →
2024-07-03 06:10
Mathlib/Geometry/RingedSpace/LocallyRingedSpace/ResidueField.lean
feat(AlgebraicGeometry): residue field of a point and evaluation (#14302) …
Added AlgebraicGeometry.LocallyRingedSpace.evaluation_naturalityView on Github →