Theorem AlgebraicGeometry.Scheme.IdealSheafData.Hom.toImageAux_spec

Modification history

2026-04-28 19:59
Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean
chore(AlgebraicGeometry/IdealSheaf): un-`private` some auxiliary definitions (#38486) …
Added AlgebraicGeometry.Scheme.IdealSheafData.Hom.toImageAux_specView on Github →