Theorem Nat.ArithmeticFunction.IsMultiplicative.nat_cast

Modification history

2024-02-10 13:10

Mathlib/NumberTheory/ArithmeticFunction.lean

chore(NumberTheory/ArithmeticFunction): remove `Nat.` part from `ArithmeticFunction` namespace (#10399) …

Deleted Nat.ArithmeticFunction.IsMultiplicative.nat_cast View on Github →

2023-05-30 06:41

Mathlib/NumberTheory/ArithmeticFunction.lean

feat: port NumberTheory.ArithmeticFunction (#4358)

Added Nat.ArithmeticFunction.IsMultiplicative.nat_cast View on Github →