Commit 2023-12-27 09:02 565cdcb2
View on Github →chore(ArithmeticFunction): add cardFactors_zero
(#9287)
- Add a
dsimp
lemmacardFactors_zero
- Make
cardFactors_one
adsimp
lemma - make
cardFactors_eq_one_iff_prime
asimp
lemma
chore(ArithmeticFunction): add cardFactors_zero
(#9287)
dsimp
lemma cardFactors_zero
cardFactors_one
a dsimp
lemmacardFactors_eq_one_iff_prime
a simp
lemma