Commit 2024-12-17 11:38 d5bed454
View on Github →faet(RingTheory/DiscreteValuationRing/Basic): rename DiscreteValuationRing to IsDiscreteValuationRing. (#19947)
In this PR we rename DiscreteValuationRing to IsDiscreteValuationRing, since the latter is Prop-valued.
Estimated changes
deleted theorem DiscreteValuationRing.HasUnitMulPowIrreducibleFactorization.of_ufd_of_unique_irreducible
deleted theorem DiscreteValuationRing.HasUnitMulPowIrreducibleFactorization.toUniqueFactorizationMonoid
added theorem IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization.of_ufd_of_unique_irreducible