Theorem AlgebraicGeometry.Scheme.Hom.residueFieldMap_congr'

Modification history

2026-06-09 19:37

Mathlib/AlgebraicGeometry/ResidueField.lean

feat(AlgebraicGeometry/Morphisms/UniversallyInjective): equivalent criteria for universally injective morphisms (#39910) …

Added AlgebraicGeometry.Scheme.Hom.residueFieldMap_congr'View on Github →