Commit 2023-05-22 18:01 e8f2fcba

View on Github →

feat: port RingTheory.DiscreteValuationRing.Basic (#4156)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/DiscreteValuationRing/Basic.lean

added theorem DiscreteValuationRing.HasUnitMulPowIrreducibleFactorization.of_ufd_of_unique_irreducible

added theorem DiscreteValuationRing.HasUnitMulPowIrreducibleFactorization.toUniqueFactorizationMonoid

added theorem DiscreteValuationRing.HasUnitMulPowIrreducibleFactorization.unique_irreducible

added def DiscreteValuationRing.HasUnitMulPowIrreducibleFactorization

added theorem DiscreteValuationRing.addVal_add

added theorem DiscreteValuationRing.addVal_def'

added theorem DiscreteValuationRing.addVal_def

added theorem DiscreteValuationRing.addVal_eq_top_iff

added theorem DiscreteValuationRing.addVal_le_iff_dvd

added theorem DiscreteValuationRing.addVal_mul

added theorem DiscreteValuationRing.addVal_one

added theorem DiscreteValuationRing.addVal_pow

added theorem DiscreteValuationRing.addVal_uniformizer

added theorem DiscreteValuationRing.addVal_zero

added theorem DiscreteValuationRing.associated_of_irreducible

added theorem DiscreteValuationRing.associated_pow_irreducible

added theorem DiscreteValuationRing.aux_pid_of_ufd_of_unique_irreducible

added theorem DiscreteValuationRing.eq_unit_mul_pow_irreducible

added theorem DiscreteValuationRing.exists_irreducible

added theorem DiscreteValuationRing.exists_prime

added theorem DiscreteValuationRing.ideal_eq_span_pow_irreducible

added theorem DiscreteValuationRing.iff_pid_with_one_nonzero_prime

added theorem DiscreteValuationRing.irreducible_iff_uniformizer

added theorem DiscreteValuationRing.irreducible_of_span_eq_maximalIdeal

added theorem DiscreteValuationRing.not_a_field

added theorem DiscreteValuationRing.not_isField

added theorem DiscreteValuationRing.ofHasUnitMulPowIrreducibleFactorization

added theorem DiscreteValuationRing.of_ufd_of_unique_irreducible

added theorem DiscreteValuationRing.unit_mul_pow_congr_pow

added theorem DiscreteValuationRing.unit_mul_pow_congr_unit

added theorem Irreducible.maximalIdeal_eq