Def AlgebraicGeometry.arrowIsoΓSpecOfIsAffine

Modification history

2024-10-11 13:11

Mathlib/AlgebraicGeometry/AffineScheme.lean

feat(AlgebraicGeometry): factorization of morphisms with affine target (#15033)

Added AlgebraicGeometry.arrowIsoΓSpecOfIsAffine View on Github →