chinese_remainder_theorem

Stream: mathlib4

[BANGJI HU]

Has this theorem been proven in mathlib?

[BANGJI HU]

Am I blacklisted?

[Yury G. Kudryashov]

docs#Nat.chineseRemainder docs#ZMod.chineseRemainder

[Kim Morrison]

hand bob said:

Am I blacklisted?

@hand bob, I suspect your problem is that people may feel that you are asking many "low effort" questions, and as such are hesitant to invest effort into replying. (Some recent posts which looks very "homework"y haven't helped.) Posting more context with your questions, especially explaining what you have already tried, should get much better results.

[Kim Morrison]

Even for this question, you could have said: "I have searched on moogle/leansearch.net/loogle and found nothing" or "I do not know how to search for proven facts, could someone explain that?"

[BANGJI HU]

is fermat little theory prooved in mathlib？

[BANGJI HU]

@Yury G. Kudryashov

[Ruben Van de Velde]

What have you tried to figure out the answer to that question?

[Yury G. Kudryashov]

Yes. Did you try any of the search engines mentioned above?

[BANGJI HU]

i have search on loogle

[BANGJI HU]

fermat number

[Yury G. Kudryashov]

Try other engines too. Also, git grep -i 'fermat.*little' helps.

[BANGJI HU]

how did you konw

[BANGJI HU]

can you please give a link

[Yury G. Kudryashov]

No, because I want you to learn how to do it yourself next time.