mathlib3
49420fb1 - chore(number_theory/arithmetic_function): golf (#17953)

Commit

3 years ago

chore(number_theory/arithmetic_function): golf (#17953) Also generalize `coe_zeta_smul_apply`.

Author

urkud

Parents