Zulip Chat Archive

Stream: mathlib4

Topic: ring

BANGJI HU (Apr 01 2025 at 09:26):

How to prove that a structure is not a ring in Lean, such as 2Zunion3Z, what definition should be used?

Damiano Testa (Apr 01 2025 at 09:58):

Intertwine with reduce_mod_char.

Anne Baanen (Apr 01 2025 at 10:52):

(I should really get working on #10765 again!)

Jz Pan (Apr 02 2025 at 08:09):

.

Andrew Yang (Apr 06 2025 at 06:10):

Please do not edit your question into something entirely different.

Yury G. Kudryashov (Apr 06 2025 at 15:02):

Please start with a detailed informal statement and proof.

Last updated: May 02 2025 at 03:31 UTC