Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-16 17:33 96667b51

View on Github →

chore(number_theory/*): Weaken assumptions (#13443) Follow @alexjbest's generalization linter to weaken typeclass assumptions in number theory.

Estimated changes

Modified src/number_theory/arithmetic_function.lean

modified theorem nat.arithmetic_function.coe_moebius_mul_coe_zeta

modified theorem nat.arithmetic_function.sum_eq_iff_sum_mul_moebius_eq

Modified src/number_theory/class_number/admissible_card_pow_degree.lean

modified theorem polynomial.exists_approx_polynomial_aux

modified theorem polynomial.exists_eq_polynomial

Modified src/number_theory/class_number/finite.lean

modified theorem class_group.norm_lt

Modified src/number_theory/liouville/basic.lean

modified theorem liouville.exists_one_le_pow_mul_dist

Modified src/number_theory/padics/ring_homs.lean

modified theorem padic_int.to_zmod_pow_eq_iff_ext

Modified src/number_theory/zsqrtd/basic.lean

modified theorem zsqrtd.hom_ext