Commit 2023-06-21 16:11 ee000bf3

View on Github →

feat: port RingTheory.Valuation.ValuationSubring (#4791)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Order/RelClasses.lean

Modified Mathlib/RingTheory/Valuation/ValuationRing.lean

Created Mathlib/RingTheory/Valuation/ValuationSubring.lean

added theorem Valuation.isEquiv_iff_valuationSubring

added theorem Valuation.isEquiv_valuation_valuationSubring

added theorem Valuation.mem_unitGroup_iff

added theorem Valuation.mem_valuationSubring_iff

added def Valuation.valuationSubring

added def ValuationSubring.ValueGroup

added theorem ValuationSubring.add_mem

added theorem ValuationSubring.algebraMap_apply

added theorem ValuationSubring.coe_comap

added theorem ValuationSubring.coe_mem_nonunits_iff

added theorem ValuationSubring.coe_mem_principalUnitGroup_iff

added theorem ValuationSubring.coe_pointwise_smul

added theorem ValuationSubring.coe_unitGroupMulEquiv_apply

added theorem ValuationSubring.coe_unitGroupMulEquiv_symm_apply

added theorem ValuationSubring.coe_unitGroupToResidueFieldUnits_apply

added def ValuationSubring.comap

added theorem ValuationSubring.comap_comap

added theorem ValuationSubring.eq_iff_principalUnitGroup

added theorem ValuationSubring.eq_iff_unitGroup

added theorem ValuationSubring.ext

added def ValuationSubring.idealOfLE

added theorem ValuationSubring.idealOfLE_le_of_le

added theorem ValuationSubring.idealOfLE_ofPrime

added theorem ValuationSubring.image_maximalIdeal

added def ValuationSubring.inclusion

added theorem ValuationSubring.ker_unitGroupToResidueFieldUnits

added theorem ValuationSubring.le_ofPrime

added theorem ValuationSubring.le_top

added def ValuationSubring.mapOfLE

added theorem ValuationSubring.mapOfLE_comp_valuation

added theorem ValuationSubring.mapOfLE_valuation_apply

added theorem ValuationSubring.mem_carrier

added theorem ValuationSubring.mem_comap

added theorem ValuationSubring.mem_inv_pointwise_smul_iff

added theorem ValuationSubring.mem_nonunits_iff

added theorem ValuationSubring.mem_nonunits_iff_exists_mem_maximalIdeal

added theorem ValuationSubring.mem_ofSubring

added theorem ValuationSubring.mem_of_valuation_le_one

added theorem ValuationSubring.mem_or_inv_mem

added theorem ValuationSubring.mem_pointwise_smul_iff_inv_smul_mem

added theorem ValuationSubring.mem_principalUnitGroup_iff

added theorem ValuationSubring.mem_smul_pointwise_iff_exists

added theorem ValuationSubring.mem_toSubring

added theorem ValuationSubring.mem_top

added theorem ValuationSubring.mem_unitGroup_iff

added theorem ValuationSubring.monotone_mapOfLE

added theorem ValuationSubring.mul_mem

added theorem ValuationSubring.neg_mem

added def ValuationSubring.nonunits

added def ValuationSubring.nonunitsOrderEmbedding

added theorem ValuationSubring.nonunits_inj

added theorem ValuationSubring.nonunits_injective

added theorem ValuationSubring.nonunits_le

added theorem ValuationSubring.nonunits_le_nonunits

added theorem ValuationSubring.nonunits_subset

added def ValuationSubring.ofLE

added def ValuationSubring.ofPrime

added theorem ValuationSubring.ofPrime_idealOfLE

added theorem ValuationSubring.ofPrime_le_of_le

added theorem ValuationSubring.ofPrime_valuation_eq_one_iff_mem_primeCompl

added def ValuationSubring.ofSubring

added theorem ValuationSubring.one_mem

added def ValuationSubring.pointwiseHasSmul

added def ValuationSubring.pointwiseMulAction

added theorem ValuationSubring.pointwise_smul_le_pointwise_smul_iff

added theorem ValuationSubring.pointwise_smul_subset_iff

added theorem ValuationSubring.pointwise_smul_toSubring

added def ValuationSubring.primeSpectrumEquiv

added def ValuationSubring.primeSpectrumOrderEquiv

added def ValuationSubring.principalUnitGroup

added def ValuationSubring.principalUnitGroupEquiv

added theorem ValuationSubring.principalUnitGroupEquiv_apply

added def ValuationSubring.principalUnitGroupOrderEmbedding

added theorem ValuationSubring.principalUnitGroup_injective

added theorem ValuationSubring.principalUnitGroup_le_principalUnitGroup

added theorem ValuationSubring.principalUnitGroup_symm_apply

added theorem ValuationSubring.principal_units_le_units

added theorem ValuationSubring.smul_mem_pointwise_smul

added theorem ValuationSubring.smul_mem_pointwise_smul_iff

added theorem ValuationSubring.subset_pointwise_smul_iff

added def ValuationSubring.subtype

added theorem ValuationSubring.surjective_unitGroupToResidueFieldUnits

added theorem ValuationSubring.toSubring_injective

added def ValuationSubring.unitGroup

added def ValuationSubring.unitGroupMulEquiv

added def ValuationSubring.unitGroupOrderEmbedding

added def ValuationSubring.unitGroupToResidueFieldUnits

added theorem ValuationSubring.unitGroup_injective

added theorem ValuationSubring.unitGroup_le_unitGroup

added theorem ValuationSubring.unitGroup_strictMono

added def ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits

added theorem ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk

added theorem ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk_apply

added def ValuationSubring.valuation

added theorem ValuationSubring.valuationSubring_valuation

added theorem ValuationSubring.valuation_eq_iff

added theorem ValuationSubring.valuation_eq_one_iff

added theorem ValuationSubring.valuation_le_iff

added theorem ValuationSubring.valuation_le_one

added theorem ValuationSubring.valuation_le_one_iff

added theorem ValuationSubring.valuation_lt_one_iff

added theorem ValuationSubring.valuation_lt_one_or_eq_one

added theorem ValuationSubring.valuation_surjective

added theorem ValuationSubring.valuation_unit

added theorem ValuationSubring.zero_mem

added structure ValuationSubring