Theorem AlgebraicGeometry.Scheme.descResidueField_stalkClosedPointTo_comp

Modification history

2026-09-04 11:59
Mathlib/AlgebraicGeometry/ResidueField.lean
chore(CategoryTheory): use the new `↧` notation in concrete categories (#41811) …
Modified AlgebraicGeometry.Scheme.descResidueField_stalkClosedPointTo_compView on Github →
2026-06-09 19:37
Mathlib/AlgebraicGeometry/ResidueField.lean
feat(AlgebraicGeometry/Morphisms/UniversallyInjective): equivalent criteria for universally injective morphisms (#39910) …
Added AlgebraicGeometry.Scheme.descResidueField_stalkClosedPointTo_compView on Github →