Documentation Verification Report

field

📁 Source: MathlibTest/grind/field.lean

Statistics

Metric	Count
Definitions `field`, `field`, `field`, `field`, `field`, `field`, `field`, `field`, `field`, `field`, `field`, `field`, `field`	13
Theorems	0
Total	13

AlgebraicGeometry.ValuativeCommSq

Definitions

Name	Category	Theorems
`field` 📖	CompOp	2 math math: `isFractionRing`, `commSq`

CauSeq.Completion.Cauchy

Definitions

Name	Category	Theorems
`field` 📖	CompOp	—

Equiv

Definitions

Name	Category	Theorems
`field` 📖	CompOp	—

Field.DirectLimit

Definitions

Name	Category	Theorems
`field` 📖	CompOp	—

FirstOrder.Language.Theory

Definitions

Name	Category	Theorems
`field` 📖	CompOp	2 math math: `FirstOrder.Field.modelField_of_modelACF`, `FirstOrder.Field.instModelField`

FractionRing

Definitions

Name	Category	Theorems
`field` 📖	CompOp	44 math math: `ClassGroup.mk0_integralRep`, `ClassGroup.mk_eq_mk_of_coe_ideal`, `ClassGroup.Quot_mk_eq_mk`, `instIsSeparableFractionRingLocalizationAlgebraMapSubmonoidPrimeCompl`, `algebraMap_liftAlgebra`, `instIsPushoutFractionRingPolynomial_1`, `coeSubmodule_differentIdeal_fractionRing`, `Ring.instIsScalarTowerSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure`, `Algebra.algebraMap_intNorm_fractionRing`, `Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure_1`, `WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_neg_mul`, `AlgebraicIndependent.lift_reprField`, `Ring.instIsFractionRingNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure`, `instIsScalarTowerAtPrimeFractionRing`, `map_equiv_traceDual`, `Ideal.relNorm_algebraMap'`, `Ring.instIsSeparableFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure`, `Ideal.relNorm_algebraMap`, `IsGaloisGroup.toFractionRing`, `WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal'`, `AlgebraicIndependent.liftAlgHom_comp_reprField`, `ClassGroup.mk_eq_mk`, `Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure`, `WeierstrassCurve.Affine.Point.toClass_some`, `Ring.instFiniteDimensionalFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure`, `instIsSeparableFractionRingAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl`, `AlgebraicIndependent.aevalEquivField_apply_coe`, `Algebra.IsAlgebraic.rank_fractionRing`, `instIsPushoutFractionRingPolynomial`, `Ring.instFaithfulSMulSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure`, `Ring.instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure`, `ClassGroup.mk_eq_one_of_coe_ideal`, `Algebra.IsAlgebraic.rank_fractionRing_mvPolynomial`, `Algebra.algebraMap_intTrace_fractionRing`, `Ideal.absNorm_algebraMap`, `Ring.instIsIntegralClosureNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure`, `Ring.instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure_1`, `Ring.instIsGaloisFractionRingNormalClosure`, `instFiniteDimensionalFractionRingOfFinite`, `Algebra.IsAlgebraic.rank_fractionRing_polynomial`, `ClassGroup.mk_def`, `WeierstrassCurve.Affine.Point.toClass_apply`, `instIsPushoutFractionRingMvPolynomial_1`, `instIsPushoutFractionRingMvPolynomial`

Function.Injective

Definitions

Name	Category	Theorems
`field` 📖	CompOp	—

Ideal.Quotient

Definitions

Name	Category	Theorems
`field` 📖	CompOp	7 math math: `IsLocalization.AtPrime.equivQuotientMapOfIsMaximal_symm_apply_mk`, `normal`, `KummerDedekind.emultiplicity_factors_map_eq_emultiplicity`, `KummerDedekind.normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map`, `Ideal.Factors.finiteDimensional_quotient_pow`, `IsLocalization.AtPrime.equivQuotMaximalIdeal_symm_apply_mk`, `NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply`

IsLocalRing.ResidueField

Definitions

Name	Category	Theorems
`field` 📖	CompOp	118 math math: `Algebra.IsUnramifiedAt.exists_primesOver_under_adjoin_eq_singleton_and_residueField_bijective`, `Algebra.instIsSeparableResidueFieldOfFormallyUnramified`, `ValuationSubring.coe_mem_principalUnitGroup_iff`, `algebraMap_residue`, `PrimeSpectrum.preimageEquivFiber_symm_apply_coe`, `IsLocalRing.finrank_CotangentSpace_eq_one_iff`, `PrimeSpectrum.residueField_specComap`, `IsLocalRing.ker_residue`, `Ideal.exists_mem_span_singleton_map_residueField_eq`, `Ideal.ker_algebraMap_residueField`, `Polynomial.fiberEquivQuotient_tmul`, `Module.rankAtStalk_eq`, `instLiesOverFiberOfIsPrime`, `IsLocalRing.finrank_cotangentSpace_eq_zero`, `PowerSeries.degree_weierstrassMod_lt`, `instIsAlgebraicResidueFieldOfIsIntegral`, `Ideal.algebraMap_quotient_residueField_mk`, `map_comp`, `instIsLocalRingTensorProductResidueFieldOfIsLocalHomRingHomAlgebraMap`, `Algebra.instFiniteResidueFieldOfQuasiFiniteAt`, `Algebra.WeaklyQuasiFiniteAt.finite_residueField`, `IsLocalRing.residue_eq_zero_iff`, `Algebra.FormallyUnramified.iff_map_maximalIdeal_eq`, `PrimeSpectrum.coe_preimageHomeomorphFiber_apply_asIdeal`, `PowerSeries.IsWeierstrassFactorization.isWeierstrassDivision`, `PrimeSpectrum.coe_preimageOrderIsoFiber_symm_apply_coe_asIdeal`, `IsLocalRing.instIsLocalHomResidueFieldRingHomResidue`, `Algebra.FormallySmooth.iff_injective_lTensor_residueField`, `Ideal.Fiber.lift_residueField_surjective`, `Ideal.algebraMap_residueField_surjective`, `IsLocalRing.finrank_CotangentSpace_eq_one`, `IsLocalRing.finrank_cotangentSpace_eq_zero_iff`, `Algebra.instFiniteResidueFieldOfFormallyUnramified`, `IsLocalRing.map_tensorProduct_mk_eq_top`, `IsLocalRing.residue_def`, `Ideal.ResidueField.ringHom_ext_iff`, `map_comp_residue`, `instIsSeparableResidueFieldOfQuotientIdeal`, `Ideal.surjectiveOnStalks_residueField`, `PrimeSpectrum.preimageEquivFiber_apply_asIdeal`, `PrimeSpectrum.mem_image_comap_basicOpen`, `instIsScalarTower_1`, `Ideal.ResidueField.liftₐ_comp_toAlgHom`, `lift_comp_residue`, `PowerSeries.IsWeierstrassFactorization.natDegree_eq_toNat_order_map`, `instIsAlgebraicQuotientIdealResidueField`, `IsLocalRing.instFiniteDimensionalResidueFieldCotangentSpaceOfIsNoetherianRing`, `Algebra.QuasiFinite.finite_fiber`, `Algebra.QuasiFinite.instFiniteResidueField`, `mapEquiv_apply`, `Ideal.ResidueField.map_algebraMap`, `algebraMap_mk`, `Ideal.ResidueField.exists_smul_eq_tmul_one`, `Algebra.isUnramifiedAt_iff_map_eq`, `PrimeSpectrum.residueField_comap`, `Algebra.instFiniteResidueFieldOfIsUnramifiedAt`, `map_map`, `map_residue`, `IsLocalRing.PrimeSpectrum.comap_residue`, `tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain`, `map_id`, `PadicInt.toZMod_eq_residueField_comp_residue`, `RingHom.SurjectiveOnStalks.residueFieldMap_bijective`, `map_id_apply`, `Algebra.IsUnramifiedAt.not_minpoly_sq_dvd`, `Algebra.instIsSeparableResidueFieldOfIsUnramifiedAt`, `instLiesOverResidueFieldBotIdeal`, `IsLocalRing.split_injective_iff_lTensor_residueField_injective`, `Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq`, `algebraMap_eq`, `IsLocalRing.finrank_cotangentSpace_le_one_iff`, `PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal`, `IsLocalRing.instIsScalarTowerResidueFieldCotangentSpace`, `Ideal.ResidueField.algHom_ext_iff`, `ValuationSubring.surjective_unitGroupToResidueFieldUnits`, `Ideal.ResidueField.lift_algebraMap`, `ValuationSubring.principalUnitGroupEquiv_apply`, `isNilpotent_tensor_residueField_iff`, `PrimeSpectrum.coe_preimageOrderIsoFiber_apply_asIdeal`, `Module.mem_support_iff_nontrivial_residueField_tensorProduct`, `finite_of_module_finite`, `ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk_apply`, `instFiniteResidueField`, `IsLocalRing.isLocalHom_residue`, `IsDiscreteValuationRing.TFAE`, `Ideal.injective_algebraMap_quotient_residueField`, `instIsScalarTower`, `instIsScalarTowerQuotientIdealResidueField`, `PowerSeries.IsWeierstrassFactorization.degree_eq_coe_lift_order_map`, `Algebra.IsUnramifiedAt.exists_notMem_forall_ne_mem_and_adjoin_eq_top`, `IsLocalRing.CotangentSpace.span_image_eq_top_iff`, `PrimeSpectrum.coe_preimageHomeomorphFiber_symm_apply_coe_asIdeal`, `Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux`, `residue_smul`, `PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply_coe`, `IsLocalRing.subsingleton_tensorProduct`, `IsLocalRing.instFiniteResidueField`, `ValuationSubring.ker_unitGroupToResidueFieldUnits`, `PrimeSpectrum.mem_image_comap_zeroLocus_sdiff`, `Polynomial.residueFieldMapCAlgEquiv_symm_X`, `Algebra.isSeparable_residueField_iff`, `Ideal.algebraMap_residueField_eq_zero`, `Ideal.bijective_algebraMap_quotient_residueField`, `Ideal.ResidueField.liftₐ_algebraMap`, `Algebra.QuasiFinite.instIsArtinianRingFiber`, `IsLocalRing.instIsScalarTowerResidueField`, `lift_residue_apply`, `Polynomial.residueFieldMapCAlgEquiv_algebraMap`, `ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk`, `ValuationSubring.coe_unitGroupToResidueFieldUnits_apply`, `Ideal.Fiber.exists_smul_eq_one_tmul`, `Valuation.HasExtension.algebraMap_residue_eq_residue_algebraMap`, `Ideal.ResidueField.mapₐ_apply`, `PrimeSpectrum.nontrivial_iff_mem_rangeComap`, `IsLocalRing.residue_surjective`, `Polynomial.residueFieldMapCAlgEquiv_symm_C`, `ValuationSubring.principalUnitGroup_symm_apply`, `instIsFractionRingQuotientIdealResidueField`

Mathlib.Tactic.FieldSimp

Definitions

Name	Category	Theorems
`field` 📖	CompOp	—

Padic

Definitions

Name	Category	Theorems
`field` 📖	CompOp	41 math math: `coe_neg`, `complete'`, `PadicComplex.coe_eq`, `coe_div`, `Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply`, `coe_sub`, `padicNormE.nonarchimedean'`, `PadicComplex.norm_def`, `padicNormE.image'`, `coe_zero`, `padicNormE.eq_padic_norm'`, `PadicInt.algebraMap_apply`, `PadicAlgCl.norm_extends`, `Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn`, `padicNormE.defn`, `padicNormE.add_eq_max_of_ne'`, `norm_p_pow`, `PadicInt.coe_adicCompletionIntegersEquiv_symm_apply`, `coe_mul`, `PadicAlgCl.instUniformContinuousConstSMulPadic`, `PadicInt.Coe.ringHom_apply`, `padicNormE.is_norm`, `PadicAlgCl.spectralNorm_eq`, `PadicInt.coe_adicCompletionIntegersEquiv_apply`, `coe_inj`, `PadicInt.isFractionRing`, `coe_one`, `PadicAlgCl.isAlgebraic`, `complete''`, `PadicComplex.instIsScalarTowerPadicPadicAlgCl`, `isAbsoluteValue`, `exi_rat_seq_conv`, `Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply`, `valuation_pow`, `rat_dense'`, `coe_add`, `PadicAlgCl.coe_eq`, `PadicInt.coe_dpow_eq`, `PadicComplexInt.integers`, `PadicInt.coe_pow`, `valuation_inv`

Polynomial.SplittingFieldAux

Definitions

Name	Category	Theorems
`field` 📖	CompOp	5 math math: `algebraMap_succ`, `adjoin_rootSet`, `scalar_tower'`, `instIsSplittingFieldNatDegree`, `splits`

ULift

Definitions

Name	Category	Theorems
`field` 📖	CompOp	—

---

← Back to Index