Commit 2025-10-06 20:40 b9b63f9b

View on Github →

chore(RingTheory): golf entire smul_eq_zero_of_mem, hasEval, eq_of_prod_eq_prod and isIntegral_of_mem_ringOfIntegers (#28487)

Estimated changes

Modified Mathlib/RingTheory/Extension/Basic.lean

Modified Mathlib/RingTheory/PowerSeries/Substitution.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean

deleted theorem Associates.eq_of_prod_eq_prod

Modified Mathlib/RingTheory/Valuation/AlgebraInstances.lean