ValuationSubring

📁 Source: Mathlib/RingTheory/Valuation/ValuationSubring.lean

Statistics

Metric	Count
Definitions valuationSubring, ValuationSubring, ValueGroup, comap, idealOfLE, inclusion, inhabitedValueGroup, instAlgebraSubtypeMem, instCommRingSubtypeMem, instFieldSubtypeMemTop, instInhabited, instLinearOrderedCommGroupWithZeroValueGroup, instOrderTop, instPartialOrder, instSemilatticeSup, instSetLike, instTop, linearOrderOverring, mapOfLE, nonunits, nonunitsOrderEmbedding, ofLE, ofPrime, ofPrimeAlgebra, ofSubring, pointwiseHasSMul, pointwiseMulAction, primeSpectrumEquiv, primeSpectrumOrderEquiv, principalUnitGroup, principalUnitGroupEquiv, principalUnitGroupOrderEmbedding, subtype, toSubring, unitGroup, unitGroupMulEquiv, unitGroupOrderEmbedding, unitGroupToResidueFieldUnits, unitsModPrincipalUnitsEquivResidueFieldUnits, valuation	40
Theorems isEquiv_iff_valuationSubring, isEquiv_valuation_valuationSubring, isNontrivial_valuation_valuationSubring_iff, mem_maximalIdeal_iff, mem_unitGroup_iff, mem_valuationSubring_iff, integers, valuationSubring_eq_top_iff, add_mem, algebraMap_apply, coe_comap, coe_mem_nonunits_iff, coe_mem_principalUnitGroup_iff, coe_pointwise_smul, coe_primeSpectrumOrderEquiv_symm_apply_asIdeal, coe_subtype, coe_unitGroupMulEquiv_apply, coe_unitGroupMulEquiv_symm_apply, coe_unitGroupToResidueFieldUnits_apply, comap_comap, eq_iff_principalUnitGroup, eq_iff_unitGroup, eq_top_iff, ext, ext_iff, idealOfLE_le_of_le, idealOfLE_ofPrime, image_maximalIdeal, instCovariantClassHSMulLe, instIsDomainSubtypeMem, instIsFractionRingSubtypeMem, instSubringClass, instValuationRingSubtypeMem, integer_valuation, inv_mem_nonunits_iff, isLocalRing, ker_unitGroupToResidueFieldUnits, le_ofPrime, le_top, le_total_ideal, mapOfLE_comp_valuation, mapOfLE_valuation_apply, mem_carrier, mem_comap, mem_inv_pointwise_smul_iff, mem_nonunits_iff, mem_nonunits_iff_exists_mem_maximalIdeal, mem_nonunits_iff_or, mem_ofSubring, mem_of_valuation_le_one, mem_or_inv_mem, mem_or_inv_mem', mem_pointwise_smul_iff_inv_smul_mem, mem_principalUnitGroup_iff, mem_smul_pointwise_iff_exists, mem_toSubring, mem_top, mem_unitGroup_iff, monotone_mapOfLE, mul_mem, neg_mem, nonunits_inj, nonunits_injective, nonunits_le, nonunits_le_nonunits, nonunits_subset, ofPrime_idealOfLE, ofPrime_le_of_le, ofPrime_localization, ofPrime_scalar_tower, ofPrime_valuation_eq_one_iff_mem_primeCompl, one_mem, pointwise_central_scalar, pointwise_smul_le_pointwise_smul_iff, pointwise_smul_subset_iff, pointwise_smul_toSubring, primeSpectrumEquiv_apply, primeSpectrumOrderEquiv_apply_coe_carrier, prime_idealOfLE, principalUnitGroupEquiv_apply, principalUnitGroup_injective, principalUnitGroup_le_principalUnitGroup, principalUnitGroup_symm_apply, principal_units_le_units, smul_mem_pointwise_smul, smul_mem_pointwise_smul_iff, subset_pointwise_smul_iff, subtype_apply, subtype_injective, surjective_unitGroupToResidueFieldUnits, toSubring_injective, toSubring_top, top_coe_div, top_coe_inv, unitGroup_injective, unitGroup_le_unitGroup, unitGroup_strictMono, unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk, unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk_apply, valuationSubring_valuation, valuation_eq_iff, valuation_eq_one_iff, valuation_le_iff, valuation_le_one, valuation_le_one_iff, valuation_lt_one_iff, valuation_lt_one_or_eq_one, valuation_surjective, valuation_unit, zero_mem	110
Total	150

Valuation

Definitions

Name	Category	Theorems
valuationSubring 📖	CompOp	48 math math: ValuationSubring.integralClosure_algebraMap_injective, mem_maximalIdeal_iff, HasExtension.instIsLocalHomSubtypeMemValuationSubringValuationSubringRingHomAlgebraMap, isEquiv_valuation_valuationSubring, Set.unit_eq, ArchimedeanClass.FiniteResidueField.mk_eq_zero, ArchimedeanClass.FiniteElement.val_add, ArchimedeanClass.FiniteElement.not_isUnit_iff_mk_pos, Valued.isClopen_valuationSubring, exists_isUniformizer_of_isCyclic_of_nontrivial, mem_unitGroup_iff, Valued.isClosed_valuationSubring, ArchimedeanClass.FiniteElement.val_mul, HasExtension.maximalIdeal_comap_algebraMap_eq_maximalIdeal, mem_valuationSubring_iff, pow_Uniformizer_is_pow_generator, ideal_isPrincipal, ValuationSubring.instIsScalarTowerSubtypeMemValuationSubringWithZeroMultiplicativeInt, ArchimedeanClass.FiniteElement.val_sub, valuationSubring_isDiscreteValuationRing, Valued.isOpen_valuationSubring, HasExtension.instIsScalarTower_valuationSubring', ArchimedeanClass.FiniteResidueField.mk_eq_mk, valuationSubring_isPrincipalIdealRing, ValuationSubring.isIntegral_of_mem_ringOfIntegers', ArchimedeanClass.FiniteElement.val_zero, IsDiscreteValuationRing.map_algebraMap_eq_valuationSubring, ArchimedeanClass.FiniteElement.isUnit_iff_mk_eq_zero, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, HasExtension.algebraMap_mem_valuationSubring, ArchimedeanClass.FiniteResidueField.mk_ne_zero, valuationSubring.integers, isNontrivial_valuation_valuationSubring_iff, ArchimedeanClass.FiniteElement.val_one, valuationSubring_not_isField, exists_pow_Uniformizer, Uniformizer.is_generator, Set.integer_eq, valuationSubring_eq_top_iff, HasExtension.instIsScalarTower_valuationSubring, HasExtension.coe_algebraMap_valuationSubring_eq, ValuationSubring.algebraMap_injective, HasExtension.instLiesOverSubtypeMemValuationSubringValuationSubringMaximalIdeal, HasExtension.algebraMap_residue_eq_residue_algebraMap, ValuationSubring.valuationSubring_valuation, ArchimedeanClass.FiniteElement.ext_iff, HasExtension.algebraMap_mem_maximalIdeal_iff, isEquiv_iff_valuationSubring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isEquiv_iff_valuationSubring 📖	mathematical	—	IsEquiv DivisionRing.toRing Field.toDivisionRing LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero valuationSubring	—	ValuationSubring.ext map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass instValuationClass isEquiv_of_val_le_one
isEquiv_valuation_valuationSubring 📖	mathematical	—	IsEquiv ValuationSubring.ValueGroup valuationSubring DivisionRing.toRing Field.toDivisionRing LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero ValuationSubring.instLinearOrderedCommGroupWithZeroValueGroup ValuationSubring.valuation	—	isEquiv_iff_val_le_one ValuationSubring.valuation_le_one_iff mem_valuationSubring_iff
isNontrivial_valuation_valuationSubring_iff 📖	mathematical	—	IsNontrivial ValuationSubring.ValueGroup valuationSubring DivisionRing.toRing Field.toDivisionRing LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero ValuationSubring.instLinearOrderedCommGroupWithZeroValueGroup ValuationSubring.valuation	—	IsEquiv.isNontrivial_iff isEquiv_valuation_valuationSubring
mem_maximalIdeal_iff 📖	mathematical	—	ValuationSubring SetLike.instMembership ValuationSubring.instSetLike valuationSubring Ideal CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing ValuationSubring.instSubringClass Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal ValuationSubring.isLocalRing Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	Integer.not_isUnit_iff_valuation_lt_one
mem_unitGroup_iff 📖	mathematical	—	Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike ValuationSubring.unitGroup valuationSubring DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DivisionRing.toRing Field.toDivisionRing instFunLike Units.val InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	IsEquiv.eq_one_iff_eq_one IsEquiv.symm isEquiv_valuation_valuationSubring
mem_valuationSubring_iff 📖	mathematical	—	ValuationSubring SetLike.instMembership ValuationSubring.instSetLike valuationSubring Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation DivisionRing.toRing Field.toDivisionRing instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	—
valuationSubring_eq_top_iff 📖	mathematical	—	valuationSubring Top.top ValuationSubring ValuationSubring.instTop IsNontrivial DivisionRing.toRing Field.toDivisionRing LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero	—	—

Valuation.valuationSubring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integers 📖	mathematical	—	Valuation.Integers Field.toCommRing ValuationSubring SetLike.instMembership ValuationSubring.instSetLike Valuation.valuationSubring ValuationSubring.instCommRingSubtypeMem ValuationSubring.instAlgebraSubtypeMem	—	Valuation.integer.integers

ValuationSubring

Definitions

Name	Category	Theorems
ValueGroup 📖	CompOp	21 math math: valuation_lt_one_iff, valuation_le_iff, Valuation.isEquiv_valuation_valuationSubring, ofPrime_valuation_eq_one_iff_mem_primeCompl, valuation_unit, mapOfLE_valuation_apply, eq_top_iff, valuation_lt_one_or_eq_one, valuation_le_one, valuation_le_one_iff, mem_unitGroup_iff, monotone_mapOfLE, valuation_eq_iff, Valuation.isNontrivial_valuation_valuationSubring_iff, mem_principalUnitGroup_iff, mem_nonunits_iff, valuation_eq_one_iff, valuation_surjective, integer_valuation, mapOfLE_comp_valuation, valuationSubring_valuation
comap 📖	CompOp	3 math math: mem_comap, coe_comap, comap_comap
idealOfLE 📖	CompOp	4 math math: idealOfLE_le_of_le, prime_idealOfLE, idealOfLE_ofPrime, ofPrime_idealOfLE
inclusion 📖	CompOp	1 math math: coe_primeSpectrumOrderEquiv_symm_apply_asIdeal
inhabitedValueGroup 📖	CompOp	—
instAlgebraSubtypeMem 📖	CompOp	9 math math: IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsScalarTower', IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers, instIsFractionRingSubtypeMem, Valuation.HasExtension.instIsScalarTower_valuationSubring', algebraMap_apply, Valuation.valuationSubring.integers, ofPrime_scalar_tower, Valuation.HasExtension.instIsScalarTower_valuationSubring, PadicComplexInt.integers
instCommRingSubtypeMem 📖	CompOp	25 math math: coe_mem_principalUnitGroup_iff, integralClosure_algebraMap_injective, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, instIsIntegrallyClosedSubtypeMemValuationSubring, IsDedekindDomain.HeightOneSpectrum.instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, Valuation.valuationSubring_isDiscreteValuationRing, PadicInt.coe_adicCompletionIntegersEquiv_apply, instValuationRingSubtypeMem, isIntegral_of_mem_ringOfIntegers', Valuation.valuationSubring.integers, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, LaurentSeries.powerSeriesRingEquiv_coe_apply, instIsDiscreteValuationRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, ofPrime_scalar_tower, surjective_unitGroupToResidueFieldUnits, principalUnitGroupEquiv_apply, unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk_apply, ker_unitGroupToResidueFieldUnits, unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk, coe_unitGroupToResidueFieldUnits_apply, Valuation.HasExtension.algebraMap_residue_eq_residue_algebraMap, PadicComplexInt.integers, principalUnitGroup_symm_apply
instFieldSubtypeMemTop 📖	CompOp	2 math math: top_coe_div, top_coe_inv
instInhabited 📖	CompOp	—
instLinearOrderedCommGroupWithZeroValueGroup 📖	CompOp	21 math math: valuation_lt_one_iff, valuation_le_iff, Valuation.isEquiv_valuation_valuationSubring, ofPrime_valuation_eq_one_iff_mem_primeCompl, valuation_unit, mapOfLE_valuation_apply, eq_top_iff, valuation_lt_one_or_eq_one, valuation_le_one, valuation_le_one_iff, mem_unitGroup_iff, monotone_mapOfLE, valuation_eq_iff, Valuation.isNontrivial_valuation_valuationSubring_iff, mem_principalUnitGroup_iff, mem_nonunits_iff, valuation_eq_one_iff, valuation_surjective, integer_valuation, mapOfLE_comp_valuation, valuationSubring_valuation
instOrderTop 📖	CompOp	—
instPartialOrder 📖	CompOp	15 math math: pointwise_smul_le_pointwise_smul_iff, principalUnitGroup_le_principalUnitGroup, primeSpectrumOrderEquiv_apply_coe_carrier, nonunits_le_nonunits, unitGroup_strictMono, pointwise_smul_subset_iff, unitGroup_le_unitGroup, le_top, instCovariantClassHSMulLe, coe_primeSpectrumOrderEquiv_symm_apply_asIdeal, le_ofPrime, ofPrime_le_of_le, subset_pointwise_smul_iff, le_total_ideal, primeSpectrumEquiv_apply
instSemilatticeSup 📖	CompOp	—
instSetLike 📖	CompOp	124 math math: mem_comap, coe_mem_principalUnitGroup_iff, valuation_lt_one_iff, image_maximalIdeal, integralClosure_algebraMap_injective, Valuation.mem_maximalIdeal_iff, mem_toSubring, mem_top, mem_or_inv_mem, valuation_le_iff, IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, Valuation.HasExtension.instIsLocalHomSubtypeMemValuationSubringValuationSubringRingHomAlgebraMap, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, ofPrime_valuation_eq_one_iff_mem_primeCompl, valuation_unit, ArchimedeanClass.FiniteResidueField.mk_eq_zero, nonunits_subset, mem_inv_pointwise_smul_iff, mem_of_valuation_le_one, Subring.exists_le_valuationSubring_of_isIntegrallyClosedIn, subtype_injective, IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsScalarTower', LaurentSeries.algebraMap_C_mem_adicCompletionIntegers, ArchimedeanClass.FiniteElement.val_add, valuation_lt_one_or_eq_one, mem_pointwise_smul_iff_inv_smul_mem, isLocalRing, smul_mem_pointwise_smul_iff, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, ArchimedeanClass.FiniteElement.not_isUnit_iff_mk_pos, LocalSubring.exists_le_valuationSubring_of_isIntegrallyClosedIn, idealOfLE_le_of_le, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply, Valued.isClopen_valuationSubring, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers, IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_mem, Valuation.exists_isUniformizer_of_isCyclic_of_nontrivial, Valued.isClosed_valuationSubring, valuation_le_one, ArchimedeanClass.FiniteElement.val_mul, Valuation.HasExtension.maximalIdeal_comap_algebraMap_eq_maximalIdeal, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, primeSpectrumOrderEquiv_apply_coe_carrier, instIsIntegrallyClosedSubtypeMemValuationSubring, Valuation.mem_valuationSubring_iff, coe_unitGroupMulEquiv_apply, Valuation.pow_Uniformizer_is_pow_generator, valuation_le_one_iff, Valuation.ideal_isPrincipal, instIsScalarTowerSubtypeMemValuationSubringWithZeroMultiplicativeInt, ArchimedeanClass.FiniteElement.val_sub, mem_carrier, IsDedekindDomain.HeightOneSpectrum.instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, Valuation.valuationSubring_isDiscreteValuationRing, Valued.isOpen_valuationSubring, PadicInt.coe_adicCompletionIntegersEquiv_apply, instIsDomainSubtypeMem, zero_mem, instIsFractionRingSubtypeMem, Valuation.HasExtension.instIsScalarTower_valuationSubring', algebraMap_apply, valuation_eq_iff, ArchimedeanClass.FiniteResidueField.mk_eq_mk, instValuationRingSubtypeMem, Valuation.valuationSubring_isPrincipalIdealRing, isIntegral_of_mem_ringOfIntegers', ext_iff, ArchimedeanClass.FiniteElement.val_zero, coe_mem_nonunits_iff, ArchimedeanClass.FiniteElement.isUnit_iff_mk_eq_zero, mem_nonunits_iff_exists_mem_maximalIdeal, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, IsDedekindDomain.HeightOneSpectrum.coe_mem_adicCompletionIntegers, top_coe_div, Valuation.HasExtension.algebraMap_mem_valuationSubring, ArchimedeanClass.FiniteResidueField.mk_ne_zero, Valuation.valuationSubring.integers, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, LaurentSeries.powerSeriesRingEquiv_coe_apply, prime_idealOfLE, instIsDiscreteValuationRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, ArchimedeanClass.FiniteElement.val_one, ofPrime_scalar_tower, inv_mem_nonunits_iff, surjective_unitGroupToResidueFieldUnits, principalUnitGroupEquiv_apply, instSubringClass, one_mem, mem_nonunits_iff_or, coe_comap, Valuation.valuationSubring_not_isField, coe_pointwise_smul, unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk_apply, coe_unitGroupMulEquiv_symm_apply, Valuation.exists_pow_Uniformizer, mem_smul_pointwise_iff_exists, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one, mem_ofSubring, instIsPrincipalIdealRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, Valuation.Uniformizer.is_generator, coe_primeSpectrumOrderEquiv_symm_apply_asIdeal, subtype_apply, valuation_eq_one_iff, ofPrime_localization, ker_unitGroupToResidueFieldUnits, Valuation.HasExtension.instIsScalarTower_valuationSubring, LaurentSeries.mem_integers_of_powerSeries, top_coe_inv, Valuation.HasExtension.coe_algebraMap_valuationSubring_eq, algebraMap_injective, IsDedekindDomain.HeightOneSpectrum.adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers, Valuation.HasExtension.instLiesOverSubtypeMemValuationSubringValuationSubringMaximalIdeal, primeSpectrumEquiv_apply, unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk, coe_unitGroupToResidueFieldUnits_apply, coe_subtype, Valuation.HasExtension.algebraMap_residue_eq_residue_algebraMap, PadicComplexInt.integers, ArchimedeanClass.FiniteElement.ext_iff, principalUnitGroup_symm_apply, IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers, Valuation.HasExtension.algebraMap_mem_maximalIdeal_iff
instTop 📖	CompOp	7 math math: mem_top, toSubring_top, eq_top_iff, top_coe_div, le_top, Valuation.valuationSubring_eq_top_iff, top_coe_inv
linearOrderOverring 📖	CompOp	—
mapOfLE 📖	CompOp	3 math math: mapOfLE_valuation_apply, monotone_mapOfLE, mapOfLE_comp_valuation
nonunits 📖	CompOp	12 math math: image_maximalIdeal, nonunits_subset, nonunits_injective, Ideal.image_subset_nonunits_valuationSubring, nonunits_le_nonunits, coe_mem_nonunits_iff, mem_nonunits_iff_exists_mem_maximalIdeal, inv_mem_nonunits_iff, mem_nonunits_iff_or, nonunits_le, mem_nonunits_iff, nonunits_inj
nonunitsOrderEmbedding 📖	CompOp	—
ofLE 📖	CompOp	—
ofPrime 📖	CompOp	8 math math: ofPrime_valuation_eq_one_iff_mem_primeCompl, ofPrime_scalar_tower, idealOfLE_ofPrime, ofPrime_localization, le_ofPrime, ofPrime_idealOfLE, ofPrime_le_of_le, primeSpectrumEquiv_apply
ofPrimeAlgebra 📖	CompOp	2 math math: ofPrime_scalar_tower, ofPrime_localization
ofSubring 📖	CompOp	1 math math: mem_ofSubring
pointwiseHasSMul 📖	CompOp	12 math math: mem_inv_pointwise_smul_iff, pointwise_smul_le_pointwise_smul_iff, mem_pointwise_smul_iff_inv_smul_mem, smul_mem_pointwise_smul_iff, pointwise_smul_toSubring, pointwise_central_scalar, pointwise_smul_subset_iff, coe_pointwise_smul, mem_smul_pointwise_iff_exists, instCovariantClassHSMulLe, smul_mem_pointwise_smul, subset_pointwise_smul_iff
pointwiseMulAction 📖	CompOp	—
primeSpectrumEquiv 📖	CompOp	1 math math: primeSpectrumEquiv_apply
primeSpectrumOrderEquiv 📖	CompOp	2 math math: primeSpectrumOrderEquiv_apply_coe_carrier, coe_primeSpectrumOrderEquiv_symm_apply_asIdeal
principalUnitGroup 📖	CompOp	11 math math: coe_mem_principalUnitGroup_iff, eq_iff_principalUnitGroup, principalUnitGroup_le_principalUnitGroup, principal_units_le_units, principalUnitGroupEquiv_apply, mem_principalUnitGroup_iff, unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk_apply, ker_unitGroupToResidueFieldUnits, unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk, principalUnitGroup_injective, principalUnitGroup_symm_apply
principalUnitGroupEquiv 📖	CompOp	2 math math: principalUnitGroupEquiv_apply, principalUnitGroup_symm_apply
principalUnitGroupOrderEmbedding 📖	CompOp	—
subtype 📖	CompOp	3 math math: subtype_injective, subtype_apply, coe_subtype
toSubring 📖	CompOp	19 math math: mem_toSubring, toSubring_top, Subring.exists_le_valuationSubring_of_isIntegrallyClosedIn, iInf_valuationSubring_superset, Ideal.image_subset_nonunits_valuationSubring, LocalSubring.eq_iInf_of_isIntegrallyClosedIn, pointwise_smul_toSubring, mem_carrier, IsLocalRing.exists_factor_valuationRing, IsDiscreteValuationRing.map_algebraMap_eq_valuationSubring, LaurentSeries.powerSeries_ext_subring, mem_or_inv_mem', toSubring_injective, nonunits_le, Subring.eq_iInf_of_isIntegrallyClosedIn, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one, Set.integer_eq, integer_valuation, instIsIntegrallyClosedSubtypeMemSubring
unitGroup 📖	CompOp	16 math math: coe_mem_principalUnitGroup_iff, Set.unit_eq, Valuation.mem_unitGroup_iff, coe_unitGroupMulEquiv_apply, unitGroup_injective, mem_unitGroup_iff, unitGroup_strictMono, unitGroup_le_unitGroup, principal_units_le_units, surjective_unitGroupToResidueFieldUnits, unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk_apply, coe_unitGroupMulEquiv_symm_apply, eq_iff_unitGroup, ker_unitGroupToResidueFieldUnits, unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk, coe_unitGroupToResidueFieldUnits_apply
unitGroupMulEquiv 📖	CompOp	4 math math: coe_mem_principalUnitGroup_iff, coe_unitGroupMulEquiv_apply, coe_unitGroupMulEquiv_symm_apply, coe_unitGroupToResidueFieldUnits_apply
unitGroupOrderEmbedding 📖	CompOp	—
unitGroupToResidueFieldUnits 📖	CompOp	5 math math: surjective_unitGroupToResidueFieldUnits, unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk_apply, ker_unitGroupToResidueFieldUnits, unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk, coe_unitGroupToResidueFieldUnits_apply
unitsModPrincipalUnitsEquivResidueFieldUnits 📖	CompOp	2 math math: unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk_apply, unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk
valuation 📖	CompOp	20 math math: valuation_lt_one_iff, valuation_le_iff, Valuation.isEquiv_valuation_valuationSubring, ofPrime_valuation_eq_one_iff_mem_primeCompl, valuation_unit, mapOfLE_valuation_apply, eq_top_iff, valuation_lt_one_or_eq_one, valuation_le_one, valuation_le_one_iff, mem_unitGroup_iff, valuation_eq_iff, Valuation.isNontrivial_valuation_valuationSubring_iff, mem_principalUnitGroup_iff, mem_nonunits_iff, valuation_eq_one_iff, valuation_surjective, integer_valuation, mapOfLE_comp_valuation, valuationSubring_valuation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_mem 📖	mathematical	ValuationSubring SetLike.instMembership instSetLike	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	Subring.add_mem
algebraMap_apply 📖	mathematical	—	DFunLike.coe RingHom ValuationSubring SetLike.instMembership instSetLike Semiring.toNonAssocSemiring CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing instSubringClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap instAlgebraSubtypeMem	—	SubringClass.toSubsemiringClass instSubringClass
coe_comap 📖	mathematical	—	SetLike.coe ValuationSubring instSetLike comap Set.preimage DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike	—	—
coe_mem_nonunits_iff 📖	mathematical	—	NonUnitalSubring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing SetLike.instMembership NonUnitalSubring.instSetLike nonunits ValuationSubring instSetLike Ideal CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing instSubringClass Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal isLocalRing	—	SubringClass.toSubsemiringClass instSubringClass isLocalRing valuation_lt_one_iff
coe_mem_principalUnitGroup_iff 📖	mathematical	—	Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike principalUnitGroup unitGroup ValuationSubring instSetLike CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing instSubringClass MonoidHom.ker IsLocalRing.ResidueField instCommRingSubtypeMem isLocalRing IsLocalRing.ResidueField.field Units.instMulOneClass Units.map RingHom.toMonoidHom Semiring.toNonAssocSemiring CommRing.toCommSemiring IsLocalRing.residue DFunLike.coe MulEquiv Subgroup.mul Units.instMul EquivLike.toFunLike MulEquiv.instEquivLike unitGroupMulEquiv	—	SubringClass.toSubsemiringClass instSubringClass isLocalRing MonoidHom.mem_ker Units.ext_iff Ideal.instIsTwoSided_1 RingHom.map_one sub_eq_zero RingHom.map_sub Ideal.Quotient.eq_zero_iff_mem valuation_lt_one_iff
coe_pointwise_smul 📖	mathematical	—	SetLike.coe ValuationSubring instSetLike pointwiseHasSMul Set Set.smulSet SMulZeroClass.toSMul MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring Field.toSemifield instSMulZeroClass MulSemiringAction.toMulDistribMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid DivisionSemiring.toSemiring	—	—
coe_primeSpectrumOrderEquiv_symm_apply_asIdeal 📖	mathematical	—	SetLike.coe Submodule ValuationSubring SetLike.instMembership instSetLike CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing instSubringClass NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.setLike PrimeSpectrum.asIdeal DFunLike.coe RelIso Preorder.toLE PartialOrder.toPreorder instPartialOrder OrderDual PrimeSpectrum OrderDual.instLE PrimeSpectrum.instPartialOrder RelIso.instFunLike RelIso.symm primeSpectrumOrderEquiv Set.preimage RingHom RingHom.instFunLike inclusion Ideal IsLocalRing.maximalIdeal isLocalRing	—	SubringClass.toSubsemiringClass instSubringClass
coe_subtype 📖	mathematical	—	DFunLike.coe RingHom ValuationSubring SetLike.instMembership instSetLike Semiring.toNonAssocSemiring CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing instSubringClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike subtype	—	SubringClass.toSubsemiringClass instSubringClass
coe_unitGroupMulEquiv_apply 📖	mathematical	—	ValuationSubring SetLike.instMembership instSetLike Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing instSubringClass DFunLike.coe MulEquiv Units DivisionSemiring.toSemiring Semifield.toDivisionSemiring Subgroup Units.instGroup Subgroup.instSetLike unitGroup Subgroup.mul Units.instMul EquivLike.toFunLike MulEquiv.instEquivLike unitGroupMulEquiv	—	SubringClass.toSubsemiringClass instSubringClass
coe_unitGroupMulEquiv_symm_apply 📖	mathematical	—	Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Units Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike unitGroup DFunLike.coe MulEquiv ValuationSubring instSetLike CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing instSubringClass Units.instMul Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm unitGroupMulEquiv	—	SubringClass.toSubsemiringClass instSubringClass
coe_unitGroupToResidueFieldUnits_apply 📖	mathematical	—	Units.val IsLocalRing.ResidueField ValuationSubring SetLike.instMembership instSetLike instCommRingSubtypeMem isLocalRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield IsLocalRing.ResidueField.field DFunLike.coe MonoidHom Units Subgroup Units.instGroup Subgroup.instSetLike unitGroup MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Units.instMulOneClass MonoidHom.instFunLike unitGroupToResidueFieldUnits RingHom HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient IsLocalRing.maximalIdeal CommRing.toCommSemiring Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing instSubringClass MulEquiv Subgroup.mul Units.instMul EquivLike.toFunLike MulEquiv.instEquivLike unitGroupMulEquiv	—	isLocalRing
comap_comap 📖	mathematical	—	comap RingHom.comp Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	—
eq_iff_principalUnitGroup 📖	mathematical	—	principalUnitGroup	—	principalUnitGroup_injective
eq_iff_unitGroup 📖	mathematical	—	unitGroup	—	unitGroup_injective
eq_top_iff 📖	mathematical	—	Top.top ValuationSubring instTop Valuation.IsNontrivial ValueGroup DivisionRing.toRing Field.toDivisionRing LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instLinearOrderedCommGroupWithZeroValueGroup valuation	—	—
ext 📖	—	ValuationSubring SetLike.instMembership instSetLike	—	—	SetLike.ext
ext_iff 📖	mathematical	—	ValuationSubring SetLike.instMembership instSetLike	—	ext
idealOfLE_le_of_le 📖	mathematical	ValuationSubring Preorder.toLE PartialOrder.toPreorder instPartialOrder	Ideal SetLike.instMembership instSetLike CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing instSubringClass Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule idealOfLE	—	SubringClass.toSubsemiringClass instSubringClass isLocalRing valuation_lt_one_iff monotone_mapOfLE not_le_of_gt mapOfLE_valuation_apply MonoidWithZeroHom.map_one
idealOfLE_ofPrime 📖	mathematical	—	idealOfLE ofPrime le_ofPrime	—	SubringClass.toSubsemiringClass instSubringClass Ideal.ext le_ofPrime IsLocalization.AtPrime.to_map_mem_maximal_iff ofPrime_localization isLocalRing
image_maximalIdeal 📖	mathematical	—	Set.image ValuationSubring SetLike.instMembership instSetLike SetLike.coe Ideal CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing instSubringClass Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal isLocalRing NonUnitalSubring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing NonUnitalSubring.instSetLike nonunits	—	Set.ext SubringClass.toSubsemiringClass instSubringClass isLocalRing
instCovariantClassHSMulLe 📖	mathematical	—	CovariantClass ValuationSubring pointwiseHasSMul Preorder.toLE PartialOrder.toPreorder instPartialOrder	—	Set.image_mono
instIsDomainSubtypeMem 📖	mathematical	—	IsDomain ValuationSubring SetLike.instMembership instSetLike CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing instSubringClass	—	SubringClass.toSubsemiringClass Subring.instSubringClass Subring.instIsDomainSubtypeMem instIsDomain
instIsFractionRingSubtypeMem 📖	mathematical	—	IsFractionRing ValuationSubring SetLike.instMembership instSetLike SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing instSubringClass instAlgebraSubtypeMem	—	SubringClass.toSubsemiringClass instSubringClass Units.isUnit nonZeroDivisors.ne_zero SubsemiringClass.nontrivial IsSimpleRing.instNontrivial DivisionRing.isSimpleRing AddSubmonoidClass.toZeroMemClass SubsemiringClass.toAddSubmonoidClass mul_one mem_or_inv_mem AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass mem_nonZeroDivisors_iff_ne_zero SubsemiringClass.noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain inv_eq_zero mul_inv_cancel₀ one_mul
instSubringClass 📖	mathematical	—	SubringClass ValuationSubring DivisionRing.toRing Field.toDivisionRing instSetLike	—	mul_mem one_mem add_mem zero_mem neg_mem
instValuationRingSubtypeMem 📖	mathematical	—	ValuationRing ValuationSubring SetLike.instMembership instSetLike instCommRingSubtypeMem instIsDomainSubtypeMem	—	instIsDomainSubtypeMem AddSubmonoidClass.toZeroMemClass SubsemiringClass.toAddSubmonoidClass SubringClass.toSubsemiringClass instSubringClass MulZeroClass.mul_zero mem_or_inv_mem Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ one_mul Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst div_one Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial inv_div
integer_valuation 📖	mathematical	—	Valuation.integer ValueGroup DivisionRing.toRing Field.toDivisionRing instLinearOrderedCommGroupWithZeroValueGroup valuation toSubring	—	valuationSubring_valuation
inv_mem_nonunits_iff 📖	mathematical	—	NonUnitalSubring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing SetLike.instMembership NonUnitalSubring.instSetLike nonunits InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring ValuationSubring instSetLike	—	mem_nonunits_iff_or inv_inv inv_eq_zero
isLocalRing 📖	mathematical	—	IsLocalRing ValuationSubring SetLike.instMembership instSetLike CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing instSubringClass	—	SubringClass.toSubsemiringClass instSubringClass ValuationRing.isLocalRing SubsemiringClass.nontrivial IsSimpleRing.instNontrivial DivisionRing.isSimpleRing ValuationRing.toPreValuationRing instIsDomainSubtypeMem instValuationRingSubtypeMem
ker_unitGroupToResidueFieldUnits 📖	mathematical	—	MonoidHom.ker Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike unitGroup Subgroup.toGroup IsLocalRing.ResidueField ValuationSubring instSetLike instCommRingSubtypeMem isLocalRing IsLocalRing.ResidueField.field Units.instMulOneClass unitGroupToResidueFieldUnits Subgroup.comap Subgroup.subtype principalUnitGroup	—	Subgroup.ext isLocalRing SubringClass.toSubsemiringClass instSubringClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass
le_ofPrime 📖	mathematical	—	ValuationSubring Preorder.toLE PartialOrder.toPreorder instPartialOrder ofPrime	—	SubringClass.toSubsemiringClass instSubringClass instIsFractionRingSubtypeMem Subalgebra.mem_toSubring Subalgebra.algebraMap_mem
le_top 📖	mathematical	—	ValuationSubring Preorder.toLE PartialOrder.toPreorder instPartialOrder Top.top instTop	—	mem_top
le_total_ideal 📖	mathematical	—	ValuationSubring Preorder.toLE PartialOrder.toPreorder instPartialOrder	—	SubringClass.toSubsemiringClass instSubringClass ValuationRing.toPreValuationRing instIsDomainSubtypeMem instValuationRingSubtypeMem LE.total RelEmbedding.total OrderDual.total_le
mapOfLE_comp_valuation 📖	mathematical	ValuationSubring Preorder.toLE PartialOrder.toPreorder instPartialOrder	ValueGroup DFunLike.coe MonoidWithZeroHom MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero instLinearOrderedCommGroupWithZeroValueGroup MonoidWithZeroHom.funLike mapOfLE Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike valuation	—	—
mapOfLE_valuation_apply 📖	mathematical	ValuationSubring Preorder.toLE PartialOrder.toPreorder instPartialOrder	DFunLike.coe MonoidWithZeroHom ValueGroup MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero instLinearOrderedCommGroupWithZeroValueGroup MonoidWithZeroHom.funLike mapOfLE Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike valuation	—	—
mem_carrier 📖	mathematical	—	Set Set.instMembership Subsemigroup.carrier MulOne.toMul MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring DivisionRing.toRing Field.toDivisionRing Submonoid.toSubsemigroup Subsemiring.toSubmonoid Subring.toSubsemiring toSubring ValuationSubring SetLike.instMembership instSetLike	—	—
mem_comap 📖	mathematical	—	ValuationSubring SetLike.instMembership instSetLike comap DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike	—	—
mem_inv_pointwise_smul_iff 📖	mathematical	—	ValuationSubring SetLike.instMembership instSetLike pointwiseHasSMul InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SMulZeroClass.toSMul MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring Field.toSemifield instSMulZeroClass MulSemiringAction.toMulDistribMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid DivisionSemiring.toSemiring	—	Set.mem_inv_smul_set_iff
mem_nonunits_iff 📖	mathematical	—	NonUnitalSubring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing SetLike.instMembership NonUnitalSubring.instSetLike nonunits ValueGroup Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instLinearOrderedCommGroupWithZeroValueGroup DFunLike.coe Valuation DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike valuation InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	—
mem_nonunits_iff_exists_mem_maximalIdeal 📖	mathematical	—	NonUnitalSubring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing SetLike.instMembership NonUnitalSubring.instSetLike nonunits ValuationSubring instSetLike Ideal CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing instSubringClass Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal isLocalRing	—	SubringClass.toSubsemiringClass instSubringClass isLocalRing nonunits_subset coe_mem_nonunits_iff
mem_nonunits_iff_or 📖	mathematical	—	NonUnitalSubring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing SetLike.instMembership NonUnitalSubring.instSetLike nonunits MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring ValuationSubring instSetLike InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield	—	valuation_le_one_iff or_congr_right' Iff.not Valuation.one_le_val_iff lt_iff_not_ge mem_nonunits_iff NonUnitalSubring.zero_mem
mem_ofSubring 📖	mathematical	Subring DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subring.instSetLike InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield	ValuationSubring instSetLike ofSubring	—	—
mem_of_valuation_le_one 📖	mathematical	ValueGroup Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instLinearOrderedCommGroupWithZeroValueGroup DFunLike.coe Valuation DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike valuation InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	ValuationSubring SetLike.instMembership instSetLike	—	instIsDomainSubtypeMem instValuationRingSubtypeMem instIsFractionRingSubtypeMem ValuationRing.mem_integer_iff
mem_or_inv_mem 📖	mathematical	—	ValuationSubring SetLike.instMembership instSetLike InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield	—	mem_or_inv_mem'
mem_or_inv_mem' 📖	mathematical	—	Set Set.instMembership Subsemigroup.carrier MulOne.toMul MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring DivisionRing.toRing Field.toDivisionRing Submonoid.toSubsemigroup Subsemiring.toSubmonoid Subring.toSubsemiring toSubring InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield	—	—
mem_pointwise_smul_iff_inv_smul_mem 📖	mathematical	—	ValuationSubring SetLike.instMembership instSetLike pointwiseHasSMul SMulZeroClass.toSMul MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring Field.toSemifield instSMulZeroClass MulSemiringAction.toMulDistribMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid DivisionSemiring.toSemiring InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Set.mem_smul_set_iff_inv_smul_mem
mem_principalUnitGroup_iff 📖	mathematical	—	Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike principalUnitGroup ValueGroup Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instLinearOrderedCommGroupWithZeroValueGroup DFunLike.coe Valuation DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike valuation SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Units.val AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	—
mem_smul_pointwise_iff_exists 📖	mathematical	—	ValuationSubring SetLike.instMembership instSetLike pointwiseHasSMul SMulZeroClass.toSMul MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring Field.toSemifield instSMulZeroClass MulSemiringAction.toMulDistribMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid DivisionSemiring.toSemiring	—	Set.mem_smul_set
mem_toSubring 📖	mathematical	—	Subring DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subring.instSetLike toSubring ValuationSubring instSetLike	—	—
mem_top 📖	mathematical	—	ValuationSubring SetLike.instMembership instSetLike Top.top instTop	—	—
mem_unitGroup_iff 📖	mathematical	—	Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike unitGroup DFunLike.coe Valuation ValueGroup LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instLinearOrderedCommGroupWithZeroValueGroup DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike valuation Units.val InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	—
monotone_mapOfLE 📖	mathematical	ValuationSubring Preorder.toLE PartialOrder.toPreorder instPartialOrder	Monotone ValueGroup SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instLinearOrderedCommGroupWithZeroValueGroup DFunLike.coe MonoidWithZeroHom MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike mapOfLE	—	SubringClass.toSubsemiringClass instSubringClass
mul_mem 📖	mathematical	ValuationSubring SetLike.instMembership instSetLike	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	Subring.mul_mem
neg_mem 📖	mathematical	ValuationSubring SetLike.instMembership instSetLike	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing	—	Subring.neg_mem
nonunits_inj 📖	mathematical	—	nonunits	—	nonunits_injective
nonunits_injective 📖	mathematical	—	ValuationSubring NonUnitalSubring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing nonunits	—	—
nonunits_le 📖	mathematical	—	NonUnitalSubring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Preorder.toLE PartialOrder.toPreorder NonUnitalSubring.instPartialOrder nonunits Subring.toNonUnitalSubring DivisionRing.toRing Field.toDivisionRing toSubring	—	valuation_le_one_iff LT.lt.le mem_nonunits_iff
nonunits_le_nonunits 📖	mathematical	—	NonUnitalSubring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Preorder.toLE PartialOrder.toPreorder NonUnitalSubring.instPartialOrder nonunits ValuationSubring instPartialOrder	—	valuation_le_one_iff not_lt Valuation.one_lt_val_iff monotone_mapOfLE
nonunits_subset 📖	mathematical	—	Set Set.instHasSubset SetLike.coe NonUnitalSubring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing NonUnitalSubring.instSetLike nonunits ValuationSubring instSetLike	—	nonunits_le
ofPrime_idealOfLE 📖	mathematical	ValuationSubring Preorder.toLE PartialOrder.toPreorder instPartialOrder	ofPrime idealOfLE prime_idealOfLE	—	ext prime_idealOfLE mul_mem valuation_le_one_iff map_inv₀ ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass inv_one inv_le_inv₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE LinearOrderedCommMonoidWithZero.toMulPosStrictMono AddSubmonoidClass.toZeroMemClass SubsemiringClass.toAddSubmonoidClass SubringClass.toSubsemiringClass instSubringClass GroupWithZero.toNontrivial Ideal.zero_mem zero_lt_one LinearOrderedCommMonoidWithZero.toZeroLeOneClass NeZero.one not_lt isLocalRing not_iff_not valuation_lt_one_iff le_ofPrime zero_mem mem_or_inv_mem AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass Ideal.one_notMem IsUnit.of_mul_eq_one SubmonoidClass.instIsDedekindFiniteMonoidSubtypeMem SubsemiringClass.toSubmonoidClass instIsDedekindFiniteMonoid Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ one_mul Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst div_one Mathlib.Tactic.FieldSimp.NF.one_eq_eval one_ne_zero inv_inv
ofPrime_le_of_le 📖	mathematical	Ideal ValuationSubring SetLike.instMembership instSetLike CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing instSubringClass Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	instPartialOrder ofPrime	—	SubringClass.toSubsemiringClass instSubringClass
ofPrime_localization 📖	mathematical	—	IsLocalization.AtPrime ValuationSubring SetLike.instMembership instSetLike SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing instSubringClass ofPrime ofPrimeAlgebra	—	SubringClass.toSubsemiringClass instSubringClass Localization.subalgebra.isLocalization_ofField Ideal.primeCompl_le_nonZeroDivisors SubsemiringClass.noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain instIsFractionRingSubtypeMem
ofPrime_scalar_tower 📖	mathematical	—	IsScalarTower ValuationSubring SetLike.instMembership instSetLike ofPrime SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing instCommRingSubtypeMem DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing instSubringClass Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule ofPrimeAlgebra Algebra.toSMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring instAlgebraSubtypeMem	—	SubringClass.toSubsemiringClass instSubringClass IsScalarTower.subalgebra' IsScalarTower.right Ideal.primeCompl_le_nonZeroDivisors SubsemiringClass.noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain instIsFractionRingSubtypeMem
ofPrime_valuation_eq_one_iff_mem_primeCompl 📖	mathematical	—	DFunLike.coe Valuation ValueGroup ofPrime LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instLinearOrderedCommGroupWithZeroValueGroup DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike valuation ValuationSubring SetLike.instMembership instSetLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass instSubringClass Submonoid.instSetLike Ideal.primeCompl	—	SubringClass.toSubsemiringClass instSubringClass IsLocalization.AtPrime.isUnit_to_map_iff ofPrime_localization valuation_eq_one_iff
one_mem 📖	mathematical	—	ValuationSubring SetLike.instMembership instSetLike AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	Subring.one_mem
pointwise_central_scalar 📖	mathematical	—	IsCentralScalar ValuationSubring pointwiseHasSMul MulOpposite MulOpposite.instGroup	—	toSubring_injective IsCentralScalar.op_smul_eq_smul Subring.pointwise_central_scalar
pointwise_smul_le_pointwise_smul_iff 📖	mathematical	—	ValuationSubring Preorder.toLE PartialOrder.toPreorder instPartialOrder pointwiseHasSMul	—	Set.smul_set_subset_smul_set_iff
pointwise_smul_subset_iff 📖	mathematical	—	ValuationSubring Preorder.toLE PartialOrder.toPreorder instPartialOrder pointwiseHasSMul InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Set.smul_set_subset_iff_subset_inv_smul_set
pointwise_smul_toSubring 📖	mathematical	—	toSubring ValuationSubring pointwiseHasSMul Subring DivisionRing.toRing Field.toDivisionRing SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Subring.pointwiseMulAction	—	—
primeSpectrumEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv PrimeSpectrum ValuationSubring SetLike.instMembership instSetLike SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing instSubringClass Preorder.toLE PartialOrder.toPreorder instPartialOrder EquivLike.toFunLike Equiv.instEquivLike primeSpectrumEquiv ofPrime PrimeSpectrum.asIdeal	—	SubringClass.toSubsemiringClass instSubringClass
primeSpectrumOrderEquiv_apply_coe_carrier 📖	mathematical	—	SetLike.coe ValuationSubring instSetLike Preorder.toLE PartialOrder.toPreorder instPartialOrder DFunLike.coe RelIso OrderDual PrimeSpectrum SetLike.instMembership SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing instSubringClass OrderDual.instLE PrimeSpectrum.instPartialOrder RelIso.instFunLike primeSpectrumOrderEquiv setOf Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule PrimeSpectrum.asIdeal Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	—
prime_idealOfLE 📖	mathematical	ValuationSubring Preorder.toLE PartialOrder.toPreorder instPartialOrder	Ideal.IsPrime SetLike.instMembership instSetLike CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing instSubringClass idealOfLE	—	Ideal.comap_isPrime SubringClass.toSubsemiringClass instSubringClass isLocalRing Ideal.IsMaximal.isPrime' IsLocalRing.maximalIdeal.isMaximal
principalUnitGroupEquiv_apply 📖	mathematical	—	ValuationSubring SetLike.instMembership instSetLike Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing instSubringClass Units Subgroup Units.instGroup Subgroup.instSetLike MonoidHom.ker IsLocalRing.ResidueField instCommRingSubtypeMem isLocalRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring IsLocalRing.ResidueField.field Units.instMulOneClass Units.map RingHom.toMonoidHom Semiring.toNonAssocSemiring CommRing.toCommSemiring IsLocalRing.residue DFunLike.coe MulEquiv principalUnitGroup Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike principalUnitGroupEquiv	—	SubringClass.toSubsemiringClass instSubringClass isLocalRing
principalUnitGroup_injective 📖	mathematical	—	ValuationSubring Subgroup Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Units.instGroup principalUnitGroup	—	—
principalUnitGroup_le_principalUnitGroup 📖	mathematical	—	Subgroup Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Units.instGroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder principalUnitGroup ValuationSubring instPartialOrder	—	inv_one inv_neg inv_eq_iff_eq_inv add_eq_zero_iff_eq_neg neg_mem one_mem valuation_le_one_iff not_lt Valuation.one_lt_val_iff add_sub_cancel_right Units.val_mk0 mem_principalUnitGroup_iff monotone_mapOfLE
principalUnitGroup_symm_apply 📖	mathematical	—	Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Units Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike principalUnitGroup DFunLike.coe MulEquiv ValuationSubring instSetLike CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing instSubringClass MonoidHom.ker IsLocalRing.ResidueField instCommRingSubtypeMem isLocalRing IsLocalRing.ResidueField.field Units.instMulOneClass Units.map RingHom.toMonoidHom Semiring.toNonAssocSemiring CommRing.toCommSemiring IsLocalRing.residue Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm principalUnitGroupEquiv	—	SubringClass.toSubsemiringClass instSubringClass isLocalRing
principal_units_le_units 📖	mathematical	—	Subgroup Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Units.instGroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder principalUnitGroup unitGroup	—	add_sub_cancel Valuation.map_one_add_of_lt
smul_mem_pointwise_smul 📖	mathematical	ValuationSubring SetLike.instMembership instSetLike	pointwiseHasSMul SMulZeroClass.toSMul MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring Field.toSemifield instSMulZeroClass MulSemiringAction.toMulDistribMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid DivisionSemiring.toSemiring	—	Set.smul_mem_smul_set
smul_mem_pointwise_smul_iff 📖	mathematical	—	ValuationSubring SetLike.instMembership instSetLike pointwiseHasSMul SMulZeroClass.toSMul MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring Field.toSemifield instSMulZeroClass MulSemiringAction.toMulDistribMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid DivisionSemiring.toSemiring	—	Set.smul_mem_smul_set_iff
subset_pointwise_smul_iff 📖	mathematical	—	ValuationSubring Preorder.toLE PartialOrder.toPreorder instPartialOrder pointwiseHasSMul InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Set.subset_smul_set_iff
subtype_apply 📖	mathematical	—	DFunLike.coe RingHom ValuationSubring SetLike.instMembership instSetLike Semiring.toNonAssocSemiring CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing instSubringClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike subtype	—	SubringClass.toSubsemiringClass instSubringClass
subtype_injective 📖	mathematical	—	ValuationSubring SetLike.instMembership instSetLike DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing instSubringClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike subtype	—	Subring.subtype_injective
surjective_unitGroupToResidueFieldUnits 📖	mathematical	—	Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike unitGroup IsLocalRing.ResidueField ValuationSubring instSetLike instCommRingSubtypeMem isLocalRing IsLocalRing.ResidueField.field DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Units.instMulOneClass MonoidHom.instFunLike unitGroupToResidueFieldUnits	—	isLocalRing IsLocalRing.surjective_units_map_of_local_ringHom Ideal.Quotient.mk_surjective SubringClass.toSubsemiringClass instSubringClass IsLocalRing.instIsLocalHomResidueFieldRingHomResidue MulEquiv.surjective
toSubring_injective 📖	mathematical	—	ValuationSubring Subring DivisionRing.toRing Field.toDivisionRing toSubring	—	—
toSubring_top 📖	mathematical	—	toSubring Top.top ValuationSubring instTop Subring DivisionRing.toRing Field.toDivisionRing Subring.instTop	—	—
top_coe_div 📖	mathematical	—	ValuationSubring SetLike.instMembership instSetLike Top.top instTop DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing instFieldSubtypeMemTop	—	—
top_coe_inv 📖	mathematical	—	ValuationSubring SetLike.instMembership instSetLike Top.top instTop InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield instFieldSubtypeMemTop	—	—
unitGroup_injective 📖	mathematical	—	ValuationSubring Subgroup Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Units.instGroup unitGroup	—	—
unitGroup_le_unitGroup 📖	mathematical	—	Subgroup Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Units.instGroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder unitGroup ValuationSubring instPartialOrder	—	add_eq_zero_iff_neg_eq neg_mem one_mem le_iff_lt_or_eq valuation_le_one_iff Valuation.map_one_add_of_lt add_neg_cancel_comm add_mem SetLike.coe_mem SubringClass.toSubsemiringClass instSubringClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass
unitGroup_strictMono 📖	mathematical	—	StrictMono ValuationSubring Subgroup Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Units.instGroup PartialOrder.toPreorder instPartialOrder Subgroup.instPartialOrder unitGroup	—	OrderEmbedding.strictMono
unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk 📖	mathematical	—	MonoidHom.comp Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike unitGroup HasQuotient.Quotient Subgroup.toGroup QuotientGroup.instHasQuotientSubgroup Subgroup.comap Subgroup.subtype principalUnitGroup IsLocalRing.ResidueField ValuationSubring instSetLike instCommRingSubtypeMem isLocalRing IsLocalRing.ResidueField.field MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.subgroupOf QuotientGroup.Quotient.group Subgroup.normal_subgroupOf Subgroup.normal_of_comm Units.instCommGroupUnits CommRing.toCommMonoid Field.toCommRing Units.instMulOneClass MonoidHomClass.toMonoidHom MulEquiv MulOne.toMul Subgroup.normal_comap Units.instMul EquivLike.toFunLike MulEquiv.instEquivLike MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass unitsModPrincipalUnitsEquivResidueFieldUnits QuotientGroup.mk' unitGroupToResidueFieldUnits	—	isLocalRing Subgroup.normal_subgroupOf Subgroup.normal_of_comm Subgroup.normal_comap MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass
unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk_apply 📖	mathematical	—	DFunLike.coe MonoidHom HasQuotient.Quotient Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike unitGroup Subgroup.toGroup QuotientGroup.instHasQuotientSubgroup Subgroup.comap Subgroup.subtype principalUnitGroup IsLocalRing.ResidueField ValuationSubring instSetLike instCommRingSubtypeMem isLocalRing IsLocalRing.ResidueField.field MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid QuotientGroup.Quotient.group Subgroup.normal_comap Subgroup.normal_of_comm Units.instCommGroupUnits CommRing.toCommMonoid Field.toCommRing Units.instMulOneClass MonoidHom.instFunLike MulEquiv.toMonoidHom unitsModPrincipalUnitsEquivResidueFieldUnits unitGroupToResidueFieldUnits	—	isLocalRing Subgroup.normal_comap Subgroup.normal_of_comm
valuationSubring_valuation 📖	mathematical	—	Valuation.valuationSubring ValueGroup instLinearOrderedCommGroupWithZeroValueGroup valuation	—	ext valuation_le_one_iff
valuation_eq_iff 📖	mathematical	—	DFunLike.coe Valuation ValueGroup LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instLinearOrderedCommGroupWithZeroValueGroup DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike valuation Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing ValuationSubring SetLike.instMembership instSetLike Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass instSubringClass	—	Quotient.eq''
valuation_eq_one_iff 📖	mathematical	—	IsUnit ValuationSubring SetLike.instMembership instSetLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing instSubringClass DFunLike.coe Valuation ValueGroup LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instLinearOrderedCommGroupWithZeroValueGroup Valuation.instFunLike valuation InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	SubringClass.toSubsemiringClass instSubringClass valuation_unit zero_ne_one NeZero.one GroupWithZero.toNontrivial Valuation.map_zero valuation_le_one_iff map_inv₀ ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass inv_one le_refl IsUnit.of_mul_eq_one SubmonoidClass.instIsDedekindFiniteMonoidSubtypeMem SubsemiringClass.toSubmonoidClass instIsDedekindFiniteMonoid Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ one_mul Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst div_one Mathlib.Tactic.FieldSimp.NF.one_eq_eval one_ne_zero
valuation_le_iff 📖	mathematical	—	ValueGroup Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instLinearOrderedCommGroupWithZeroValueGroup DFunLike.coe Valuation DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike valuation Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing ValuationSubring SetLike.instMembership instSetLike	—	—
valuation_le_one 📖	mathematical	—	ValueGroup Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instLinearOrderedCommGroupWithZeroValueGroup DFunLike.coe Valuation DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike valuation ValuationSubring SetLike.instMembership instSetLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	instIsDomainSubtypeMem instValuationRingSubtypeMem instIsFractionRingSubtypeMem ValuationRing.mem_integer_iff
valuation_le_one_iff 📖	mathematical	—	ValueGroup Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instLinearOrderedCommGroupWithZeroValueGroup DFunLike.coe Valuation DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike valuation InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationSubring SetLike.instMembership instSetLike	—	mem_of_valuation_le_one valuation_le_one
valuation_lt_one_iff 📖	mathematical	—	ValuationSubring SetLike.instMembership instSetLike Ideal CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing instSubringClass Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal isLocalRing ValueGroup Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instLinearOrderedCommGroupWithZeroValueGroup DFunLike.coe Valuation Valuation.instFunLike valuation InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	SubringClass.toSubsemiringClass instSubringClass isLocalRing IsLocalRing.mem_maximalIdeal valuation_eq_one_iff LE.le.lt_iff_ne valuation_le_one
valuation_lt_one_or_eq_one 📖	mathematical	—	ValueGroup Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instLinearOrderedCommGroupWithZeroValueGroup DFunLike.coe Valuation DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike valuation ValuationSubring SetLike.instMembership instSetLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	lt_or_eq_of_le valuation_le_one
valuation_surjective 📖	mathematical	—	ValueGroup DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instLinearOrderedCommGroupWithZeroValueGroup DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike valuation	—	Quot.mk_surjective
valuation_unit 📖	mathematical	—	DFunLike.coe Valuation ValueGroup LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instLinearOrderedCommGroupWithZeroValueGroup DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike valuation ValuationSubring SetLike.instMembership instSetLike Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass instSubringClass InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	SubringClass.toSubsemiringClass instSubringClass Valuation.map_one valuation_eq_iff mul_one
zero_mem 📖	mathematical	—	ValuationSubring SetLike.instMembership instSetLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	Subring.zero_mem

(root)

Definitions

Name	Category	Theorems
ValuationSubring 📖	CompData	146 math math: ValuationSubring.mem_comap, ValuationSubring.coe_mem_principalUnitGroup_iff, ValuationSubring.valuation_lt_one_iff, ValuationSubring.image_maximalIdeal, ValuationSubring.integralClosure_algebraMap_injective, Valuation.mem_maximalIdeal_iff, ValuationSubring.mem_toSubring, ValuationSubring.mem_top, ValuationSubring.mem_or_inv_mem, ValuationSubring.valuation_le_iff, IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, Valuation.HasExtension.instIsLocalHomSubtypeMemValuationSubringValuationSubringRingHomAlgebraMap, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, ValuationSubring.ofPrime_valuation_eq_one_iff_mem_primeCompl, ValuationSubring.valuation_unit, ArchimedeanClass.FiniteResidueField.mk_eq_zero, ValuationSubring.nonunits_subset, ValuationSubring.mem_inv_pointwise_smul_iff, ValuationSubring.toSubring_top, ValuationSubring.mem_of_valuation_le_one, Subring.exists_le_valuationSubring_of_isIntegrallyClosedIn, ValuationSubring.subtype_injective, IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsScalarTower', ValuationSubring.pointwise_smul_le_pointwise_smul_iff, ValuationSubring.eq_top_iff, LaurentSeries.algebraMap_C_mem_adicCompletionIntegers, ArchimedeanClass.FiniteElement.val_add, ValuationSubring.valuation_lt_one_or_eq_one, ValuationSubring.mem_pointwise_smul_iff_inv_smul_mem, ValuationSubring.isLocalRing, ValuationSubring.smul_mem_pointwise_smul_iff, ValuationSubring.nonunits_injective, iInf_valuationSubring_superset, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, ArchimedeanClass.FiniteElement.not_isUnit_iff_mk_pos, LocalSubring.exists_le_valuationSubring_of_isIntegrallyClosedIn, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply, Valued.isClopen_valuationSubring, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers, IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_mem, Valuation.exists_isUniformizer_of_isCyclic_of_nontrivial, Valued.isClosed_valuationSubring, ValuationSubring.toLocalSubring_injective, ValuationSubring.valuation_le_one, ValuationSubring.principalUnitGroup_le_principalUnitGroup, ArchimedeanClass.FiniteElement.val_mul, LocalSubring.eq_iInf_of_isIntegrallyClosedIn, Valuation.HasExtension.maximalIdeal_comap_algebraMap_eq_maximalIdeal, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, ValuationSubring.primeSpectrumOrderEquiv_apply_coe_carrier, instIsIntegrallyClosedSubtypeMemValuationSubring, Valuation.mem_valuationSubring_iff, ValuationSubring.coe_unitGroupMulEquiv_apply, ValuationSubring.unitGroup_injective, Valuation.pow_Uniformizer_is_pow_generator, ValuationSubring.valuation_le_one_iff, Valuation.ideal_isPrincipal, ValuationSubring.instIsScalarTowerSubtypeMemValuationSubringWithZeroMultiplicativeInt, ValuationSubring.pointwise_smul_toSubring, ArchimedeanClass.FiniteElement.val_sub, ValuationSubring.mem_carrier, IsDedekindDomain.HeightOneSpectrum.instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, Valuation.valuationSubring_isDiscreteValuationRing, ValuationSubring.pointwise_central_scalar, Valued.isOpen_valuationSubring, ValuationSubring.nonunits_le_nonunits, PadicInt.coe_adicCompletionIntegersEquiv_apply, ValuationSubring.instIsDomainSubtypeMem, ValuationSubring.unitGroup_strictMono, ValuationSubring.zero_mem, ValuationSubring.instIsFractionRingSubtypeMem, Valuation.HasExtension.instIsScalarTower_valuationSubring', ValuationSubring.algebraMap_apply, ValuationSubring.valuation_eq_iff, ArchimedeanClass.FiniteResidueField.mk_eq_mk, ValuationSubring.instValuationRingSubtypeMem, Valuation.valuationSubring_isPrincipalIdealRing, ValuationSubring.isIntegral_of_mem_ringOfIntegers', ValuationSubring.ext_iff, ArchimedeanClass.FiniteElement.val_zero, ValuationSubring.pointwise_smul_subset_iff, ValuationSubring.coe_mem_nonunits_iff, ArchimedeanClass.FiniteElement.isUnit_iff_mk_eq_zero, ValuationSubring.mem_nonunits_iff_exists_mem_maximalIdeal, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, ValuationSubring.unitGroup_le_unitGroup, IsDedekindDomain.HeightOneSpectrum.coe_mem_adicCompletionIntegers, ValuationSubring.top_coe_div, Valuation.HasExtension.algebraMap_mem_valuationSubring, ArchimedeanClass.FiniteResidueField.mk_ne_zero, Valuation.valuationSubring.integers, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, LaurentSeries.powerSeriesRingEquiv_coe_apply, instIsDiscreteValuationRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, ArchimedeanClass.FiniteElement.val_one, ValuationSubring.ofPrime_scalar_tower, ValuationSubring.inv_mem_nonunits_iff, ValuationSubring.surjective_unitGroupToResidueFieldUnits, ValuationSubring.principalUnitGroupEquiv_apply, ValuationSubring.instSubringClass, ValuationSubring.one_mem, ValuationSubring.mem_nonunits_iff_or, ValuationSubring.coe_comap, Valuation.valuationSubring_not_isField, ValuationSubring.toSubring_injective, ValuationSubring.coe_pointwise_smul, ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk_apply, ValuationSubring.coe_unitGroupMulEquiv_symm_apply, Valuation.exists_pow_Uniformizer, ValuationSubring.le_top, ValuationSubring.mem_smul_pointwise_iff_exists, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one, ValuationSubring.mem_ofSubring, instIsPrincipalIdealRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, ValuationSubring.instCovariantClassHSMulLe, Valuation.Uniformizer.is_generator, ValuationSubring.coe_primeSpectrumOrderEquiv_symm_apply_asIdeal, ValuationSubring.subtype_apply, Subring.eq_iInf_of_isIntegrallyClosedIn, ValuationSubring.valuation_eq_one_iff, Valuation.valuationSubring_eq_top_iff, ValuationSubring.ofPrime_localization, ValuationSubring.le_ofPrime, ValuationSubring.ker_unitGroupToResidueFieldUnits, Valuation.HasExtension.instIsScalarTower_valuationSubring, LaurentSeries.mem_integers_of_powerSeries, ValuationSubring.top_coe_inv, ValuationSubring.subset_pointwise_smul_iff, ValuationSubring.le_total_ideal, Valuation.HasExtension.coe_algebraMap_valuationSubring_eq, ValuationSubring.algebraMap_injective, IsDedekindDomain.HeightOneSpectrum.adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers, Valuation.HasExtension.instLiesOverSubtypeMemValuationSubringValuationSubringMaximalIdeal, ValuationSubring.primeSpectrumEquiv_apply, ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk, ValuationSubring.coe_unitGroupToResidueFieldUnits_apply, ValuationSubring.coe_subtype, Valuation.HasExtension.algebraMap_residue_eq_residue_algebraMap, ValuationSubring.principalUnitGroup_injective, PadicComplexInt.integers, ArchimedeanClass.FiniteElement.ext_iff, ValuationSubring.principalUnitGroup_symm_apply, IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers, Valuation.HasExtension.algebraMap_mem_maximalIdeal_iff

---

← Back to Index