Theorem ArithmeticFunction.IsMultiplicative.map_div_of_coprime

Modification history

2025-04-09 00:36

Mathlib/NumberTheory/ArithmeticFunction.lean

feat: generalize Mathlib.NumberTheory (#23187) …

Modified ArithmeticFunction.IsMultiplicative.map_div_of_coprime View on Github →

2024-12-19 17:17

Mathlib/NumberTheory/ArithmeticFunction.lean

feat(NumberTheory/ArithmeticFunction): Miscellaneous lemmas about multiplicative arithmetic functions (#20025) …

Added ArithmeticFunction.IsMultiplicative.map_div_of_coprime View on Github →