Theorem AlgebraicGeometry.IsLocalAtSource.sigmaDesc

Modification history

2025-10-07 21:16
Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
chore(AlgebraicGeometry): replace `IsLocalAtTarget` by `IsZariskiLocalAtTarget` (#30310) …
Deleted AlgebraicGeometry.IsLocalAtSource.sigmaDescView on Github →
2025-04-03 11:07
Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
feat(AlgebraicGeometry): faithfully flat morphisms are topological quotient maps (#23608)
Added AlgebraicGeometry.IsLocalAtSource.sigmaDescView on Github →