Documentation Verification Report

Defs

📁 Source: Mathlib/RingTheory/LocalRing/ResidueField/Defs.lean

Statistics

Metric	Count
Definitions `instCommRingResidueField`, `instInhabitedResidueField`, `residue`	3
Theorems	0
Total	3

IsLocalRing

Definitions

Name	Category	Theorems
`instCommRingResidueField` 📖	CompOp	57 math math: `Algebra.instIsSeparableResidueFieldOfFormallyUnramified`, `Polynomial.fiberEquivQuotient_tmul`, `Module.rankAtStalk_eq`, `instIsAlgebraicResidueFieldOfIsIntegral`, `Algebra.QuasiFinite.instResidueField`, `instIsLocalRingTensorProductResidueFieldOfIsLocalHomRingHomAlgebraMap`, `Algebra.instFiniteResidueFieldOfQuasiFiniteAt`, `Algebra.WeaklyQuasiFiniteAt.finite_residueField`, `RingHom.EssFiniteType.residueFieldMap`, `residue_eq_zero_iff`, `Algebra.IsUnramifiedAt.residueField`, `Algebra.FormallyUnramified.iff_map_maximalIdeal_eq`, `Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange_residueField`, `instEssFiniteTypeResidueField_1`, `Algebra.FormallySmooth.iff_injective_lTensor_residueField`, `Ideal.Fiber.lift_residueField_surjective`, `Algebra.instFiniteResidueFieldOfFormallyUnramified`, `map_tensorProduct_mk_eq_top`, `Algebra.instFormallyUnramifiedResidueField_1`, `instIsSeparableResidueFieldOfQuotientIdeal`, `Ideal.surjectiveOnStalks_residueField`, `PrimeSpectrum.mem_image_comap_basicOpen`, `ResidueField.mapEquiv_refl`, `AlgebraicGeometry.LocallyRingedSpace.residue_comp_residueFieldMap_eq_stalkMap_comp_residue`, `Algebra.QuasiFinite.finite_fiber`, `Algebra.QuasiFinite.instFiniteResidueField`, `ResidueField.mapEquiv_apply`, `AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom_assoc`, `Ideal.ResidueField.exists_smul_eq_tmul_one`, `Algebra.isUnramifiedAt_iff_map_eq`, `Algebra.instFiniteResidueFieldOfIsUnramifiedAt`, `Algebra.instIsSeparableResidueFieldOfIsUnramifiedAt`, `split_injective_iff_lTensor_residueField_injective`, `AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv`, `instEssFiniteTypeResidueField`, `ResidueField.mapEquiv_trans`, `isNilpotent_tensor_residueField_iff`, `Module.mem_support_iff_nontrivial_residueField_tensorProduct`, `ResidueField.finite_of_module_finite`, `instFiniteResidueField`, `ResidueField.mapAut_apply`, `instIsScalarTowerQuotientIdealResidueField`, `AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv_assoc`, `subsingleton_tensorProduct`, `instFiniteResidueField`, `PrimeSpectrum.mem_image_comap_zeroLocus_sdiff`, `WeierstrassCurve.isGoodReduction_iff_isElliptic_reduction`, `Polynomial.residueFieldMapCAlgEquiv_symm_X`, `Algebra.isSeparable_residueField_iff`, `Ideal.algebraMap_residueField_eq_zero`, `Polynomial.residueFieldMapCAlgEquiv_algebraMap`, `Ideal.Fiber.exists_smul_eq_one_tmul`, `AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom`, `PrimeSpectrum.nontrivial_iff_mem_rangeComap`, `Polynomial.residueFieldMapCAlgEquiv_symm_C`, `ResidueField.mapEquiv.symm`, `Algebra.instFormallyUnramifiedResidueField`
`instInhabitedResidueField` 📖	CompOp	—
`residue` 📖	CompOp	24 math math: `ValuationSubring.coe_mem_principalUnitGroup_iff`, `ResidueField.algebraMap_residue`, `ker_residue`, `PowerSeries.degree_weierstrassMod_lt`, `residue_eq_zero_iff`, `PowerSeries.IsWeierstrassFactorization.isWeierstrassDivision`, `instIsLocalHomResidueFieldRingHomResidue`, `residue_def`, `ResidueField.map_comp_residue`, `AlgebraicGeometry.LocallyRingedSpace.residue_comp_residueFieldMap_eq_stalkMap_comp_residue`, `ResidueField.lift_comp_residue`, `PowerSeries.IsWeierstrassFactorization.natDegree_eq_toNat_order_map`, `ResidueField.map_residue`, `PrimeSpectrum.comap_residue`, `PadicInt.toZMod_eq_residueField_comp_residue`, `ResidueField.algebraMap_eq`, `ValuationSubring.principalUnitGroupEquiv_apply`, `isLocalHom_residue`, `PowerSeries.IsWeierstrassFactorization.degree_eq_coe_lift_order_map`, `ResidueField.residue_smul`, `ResidueField.lift_residue_apply`, `Valuation.HasExtension.algebraMap_residue_eq_residue_algebraMap`, `residue_surjective`, `ValuationSubring.principalUnitGroup_symm_apply`

---

← Back to Index