Type Error

Stream: new members

[Nick_adfor]

import Mathlib

example (R : Type*) [ring R] [is_noncomm_ring R] {n : ℕ} (hn : n > 2)
  (h_pow : ∀ (x : R), x^n = x) : ∀ (x y : R), x * y^(n-1) = y^(n-1) * x := by sorry

[Nick_adfor]

The code is too long to read from left to right. How can I get it shorter with more lines so that it can be easily read on Android?

[Julian Berman]

Welcome. Please have a look at #mwe, you should be able to clean that up a bit so it's easier for someone to read (and to try out) even on Android I think.

[Edward van de Meent]

This looks like lean3? Did you write this?

[Nick_adfor]

I cannot tell the difference between lean3 and lean4. When I referred to MIL, I cannot find the error.

[Ruben Van de Velde]

Where does the code come from?

[Nick_adfor]

Comes from my attempt to formalize the math problem. Now it seems to have already shown the math problen for human, but not for lean.

[Riccardo Brasca]

Where did you find the name is_noncomm_ring?

[Nick_adfor]

Riccardo Brasca said:

Where did you find the name is_noncomm_ring?

Oh...I've used an inexistent theorem.

[suhr]

Asking ChatGPT to generate your code is not a good way to learn. I would instead recommend reading Theorem Proving in Lean 4 and Mathlib4 documentation.

Answering your original question, just insert some line breaks, like so:

import Mathlib

example
    (R: Type*)
    [Ring R]
    {n: ℕ}
    (hn: n > 2)
    (h_pow: ∀x: R, x^n = x)
    : ∀x y: R,
      x * y^(n-1) = y^(n-1) * x :=
  by
    sorry

[suhr]

Indentation rules in Lean are very lax, so you can even write code in ATS3 style:

import
Mathlib

example
(R
:
Type*)
[Ring
R]
{n
:
ℕ}
(hn
:
n > 2)
(h_pow
:
∀x
:
R,
x^n
=
x)
: ∀x y
  :
  R,
  x
  *
  y^(n-1)
  =
  y^(n-1)
  *
  x
:=
by
  sorry

[Edward van de Meent]

Please don't tho

[Nick_adfor]

suhr said:

Asking ChatGPT to generate your code is not a good way to learn. I would instead recommend reading Theorem Proving in Lean 4 and Mathlib4 documentation.

Answering your original question, just insert some line breaks, like so:

import Mathlib

example
    (R: Type*)
    [Ring R]
    {n: ℕ}
    (hn: n > 2)
    (h_pow: ∀x: R, x^n = x)
    : ∀x y: R,
      x * y^(n-1) = y^(n-1) * x :=
  by
    sorry

Thank you for your advice! But my original problem is to prove the maths problem in noncomm_ring, not ring. But you do inspire me an error that "ring" should be "Ring". I do not know Lean is so case-sensitive.

Together with the advice above by Riccardo Brasca, my code can be corrected as follows

class noncomm_ring (R : Type*) extends Ring R where
(noncomm : ∃ (x y : R), x * y ≠ y * x)

example (R : Type*) [noncomm_ring R] {n : ℕ} (hn : n > 2)
  (h_pow : ∀ (x : R), x^n = x) : ∀ (x y : R), x * y^(n-1) = y^(n-1) * x := by sorry

There is no ChatGPT here. Because it is forbidden in my country : (

[Nick_adfor]

The code is too long to read from left to right. How can I get it shorter with more lines so that it can be easily read?

[Nick_adfor]

Edward van de Meent said:

Please don't tho

You seemed to lose some words : (

[Aaron Liu]

Nick_adfor said:

Thank you for your advice! But my original problem is to prove the maths problem in noncomm_ring, not ring.

docs#Ring is a not necessarily commutative ring, and docs#CommRing is a commutative ring.

[Nick_adfor]

Aaron Liu said:

Nick_adfor said:

Thank you for your advice! But my original problem is to prove the maths problem in noncomm_ring, not ring.

docs#Ring is a not necessarily commutative ring, and docs#CommRing is a commutative ring.

Oh, this must be my math mistake. It just clicked to me that mathematicians usually think that Ring is not necessarily commutative. Lean also thinks that!

[suhr]

There is no ChatGPT here. Because it is forbidden in my country : (

Which country by the way? Someone might know your native language and answer you in this language.