Skip to content

Commit ffe06c9

Browse files
doc(AlgebraicGeometry/RationalMap): fix module docstring (leanprover-community#39295)
`RationalMap.toPartialMap` only needs reduced, not integral.
1 parent c49a048 commit ffe06c9

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Mathlib/AlgebraicGeometry/RationalMap.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ public import Mathlib.AlgebraicGeometry.Morphisms.Separated
2424
Given `S`-schemes `X` and `Y` such that `Y` is locally of finite type and `X` is integral,
2525
`S`-morphisms `Spec K(X) ⟶ Y` correspond bijectively to `S`-rational maps from `X` to `Y`.
2626
* `AlgebraicGeometry.Scheme.RationalMap.toPartialMap`:
27-
If `X` is integral and `Y` is separated, then any `f : X ⤏ Y` can be realized as a partial
27+
If `X` is reduced and `Y` is separated, then any `f : X ⤏ Y` can be realized as a partial
2828
map on `f.domain`, the domain of definition of `f`.
2929
-/
3030

0 commit comments

Comments
 (0)