Commit 2024-06-22 13:56 5c1bf5e7

chore(AlgebraicGeometry): Fix wrong names (#14021) PrimeSpectrum.IsPrime -> PrimeSpectrum.isPrime PrimeSpectrum.vanishingIdeal_univ -> PrimeSpectrum.vanishingIdeal_empty isAffineAffineScheme -> isAffine_affineScheme SpecIsAffine -> isAffine_Spec isAffineOfIso -> isAffine_of_isIso rangeIsAffineOpenOfOpenImmersion -> isAffineOpen_opensRange topIsAffineOpen -> isAffineOpen_top Scheme.affineCoverIsAffine -> Scheme.isAffine_affineCover Scheme.affineBasisCoverIsAffine -> Scheme.isAffine_affineBasisCover IsAffineOpen.fromSpec_range -> IsAffineOpen.range_fromSpec IsAffineOpen.imageIsOpenImmersion -> IsAffineOpen.image_of_isOpenImmersion Scheme.quasi_compact_of_affine -> Scheme.compactSpace_of_isAffine IsAffineOpen.fromSpec_base_preimage -> IsAffineOpen.fromSpec_preimage_self IsAffineOpen.fromSpec_map_basicOpen' -> IsAffineOpen.fromSpec_preimage_basicOpen' IsAffineOpen.fromSpec_map_basicOpen -> IsAffineOpen.fromSpec_preimage_basicOpen IsAffineOpen.opensFunctor_map_basicOpen -> IsAffineOpen.fromSpec_image_basicOpen IsAffineOpen.basicOpenIsAffine -> IsAffineOpen.basicOpen IsAffineOpen.mapRestrictBasicOpen -> IsAffineOpen.ιOpens_preimage AffineTargetMorphismProperty.IsLocal.targetAffineLocallyIsLocal -> AffineTargetMorphismProperty.IsLocal.targetAffineLocally_isLocal AffineTargetMorphismProperty.IsLocal.targetAffineLocallyPullbackFstOfRightOfStableUnderBaseChange -> AffineTargetMorphismProperty.IsLocal.targetAffineLocally_pullback_fst_of_right_of_stableUnderBaseChange diagonalTargetAffineLocallyOfOpenCover -> diagonal_targetAffineLocally_of_openCover AffineTargetMorphismProperty.diagonalOfTargetAffineLocally -> AffineTargetMorphismProperty.diagonal_of_targetAffineLocally universallyIsLocalAtTarget -> universally_isLocalAtTarget universallyIsLocalAtTargetOfMorphismRestrict -> universally_isLocalAtTarget_of_morphismRestrict bot_isAffineOpen -> isAffineOpen_bot isOpenImmersion_is_local_at_target -> isOpenImmersion_isLocalAtTarget QuasiCompact.is_local_at_target -> QuasiCompact.isLocalAtTarget QuasiSeparated.is_local_at_target -> QuasiSeparated.isLocalAtTarget universallyClosed_is_local_at_target -> universallyClosed_isLocalAtTarget isReducedOfStalkIsReduced -> isReduced_of_isReduced_stalk stalk_isReduced_of_reduced -> isReduced_stalk_of_isReduced isReducedOfOpenImmersion -> isReduced_of_isOpenImmersion isReducedOfIsAffineIsReduced -> isReduced_of_isAffine_isReduced isReducedOfIsIntegral -> isReduced_of_isIntegral is_irreducible_of_isIntegral -> irreducibleSpace_of_isIntegral isIntegralOfIsIrreducibleIsReduced -> isIntegral_of_irreducibleSpace_of_isReduced isIntegral_iff_is_irreducible_and_isReduced -> isIntegral_iff_irreducibleSpace_and_isReduced isIntegralOfOpenImmersion -> isIntegral_of_isOpenImmersion isIntegralOfIsAffineIsDomain -> isIntegral_of_isAffine_of_isDomain