Commit 2023-12-27 09:02 565cdcb2
View on Github →chore(ArithmeticFunction): add cardFactors_zero (#9287)
- Add a
dsimplemmacardFactors_zero - Make
cardFactors_oneadsimplemma - make
cardFactors_eq_one_iff_primeasimplemma
chore(ArithmeticFunction): add cardFactors_zero (#9287)
dsimp lemma cardFactors_zerocardFactors_one a dsimp lemmacardFactors_eq_one_iff_prime a simp lemma