Theorem AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_symm_apply

Modification history

2026-02-12 15:58
Mathlib/AlgebraicGeometry/IdealSheaf/Basic.lean
feat(AlgebraicGeometry): `Semiring` structure on ideal sheaves (#34935)
Added AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_symm_applyView on Github →