Commit 2020-12-04 06:35 4f5046dd

View on Github →

feat(ring_theory/polynomial/cyclotomic): Möbius inversion formula for cyclotomic polynomials (#5192) Proves Möbius inversion for functions to a comm_group_with_zero Proves the Möbius inversion formula for cyclotomic polynomials

Estimated changes

Modified src/number_theory/arithmetic_function.lean

added theorem nat.arithmetic_function.prod_eq_iff_prod_pow_moebius_eq_of_nonzero

Modified src/ring_theory/polynomial/cyclotomic.lean

added theorem polynomial.cyclotomic_eq_prod_X_pow_sub_one_pow_moebius