Commit 2021-10-03 11:42 cff99277

View on Github →

refactor(ring_theory/unique_factorization_domain): rename unique_factorization_monoid.factors (#9503) This frees up the name for the non-normalizing version.

Estimated changes

Modified src/algebra/squarefree.lean

deleted theorem unique_factorization_monoid.squarefree_iff_nodup_factors

added theorem unique_factorization_monoid.squarefree_iff_nodup_normalized_factors

Modified src/field_theory/splitting_field.lean

Modified src/number_theory/arithmetic_function.lean

Modified src/ring_theory/dedekind_domain.lean

deleted theorem factors_prod_factors_eq_factors

added theorem normalized_factors_prod

deleted theorem prod_factors_eq_self

added theorem prod_normalized_factors_eq_self

modified theorem sup_eq_prod_inf_factors

Modified src/ring_theory/int/basic.lean

modified theorem nat.factors_eq

Modified src/ring_theory/unique_factorization_domain.lean

deleted theorem unique_factorization_monoid.dvd_iff_factors_le_factors

added theorem unique_factorization_monoid.dvd_iff_normalized_factors_le_normalized_factors

deleted theorem unique_factorization_monoid.dvd_of_mem_factors

added theorem unique_factorization_monoid.dvd_of_mem_normalized_factors

deleted theorem unique_factorization_monoid.exists_mem_factors_of_dvd

added theorem unique_factorization_monoid.exists_mem_normalized_factors_of_dvd

deleted theorem unique_factorization_monoid.factors_irreducible

deleted theorem unique_factorization_monoid.factors_mul

deleted theorem unique_factorization_monoid.factors_one

deleted theorem unique_factorization_monoid.factors_pow

deleted theorem unique_factorization_monoid.factors_prod

deleted theorem unique_factorization_monoid.factors_zero

deleted theorem unique_factorization_monoid.irreducible_of_factor

added theorem unique_factorization_monoid.irreducible_of_normalized_factor

deleted theorem unique_factorization_monoid.le_multiplicity_iff_repeat_le_factors

added theorem unique_factorization_monoid.le_multiplicity_iff_repeat_le_normalized_factors

deleted theorem unique_factorization_monoid.multiplicity_eq_count_factors

added theorem unique_factorization_monoid.multiplicity_eq_count_normalized_factors

deleted theorem unique_factorization_monoid.normalize_factor

added theorem unique_factorization_monoid.normalize_normalized_factor

added theorem unique_factorization_monoid.normalized_factors_irreducible

added theorem unique_factorization_monoid.normalized_factors_mul

added theorem unique_factorization_monoid.normalized_factors_one

added theorem unique_factorization_monoid.normalized_factors_pow

added theorem unique_factorization_monoid.normalized_factors_prod

added theorem unique_factorization_monoid.normalized_factors_zero

deleted theorem unique_factorization_monoid.prime_of_factor

added theorem unique_factorization_monoid.prime_of_normalized_factor

deleted theorem unique_factorization_monoid.zero_not_mem_factors

added theorem unique_factorization_monoid.zero_not_mem_normalized_factors