Commring cannot be inferred automatically.

Stream: new members

[Hbz]

import Mathlib

open Polynomial
noncomputable section
def quotientRing (F : Type _) [Field F] : Type _ :=
  let A : Type _ := Polynomial F  -- 单变量多项式环 F[y]
  let B : Type _ := Polynomial A  -- 二元多项式环 F[x,y] (x为外层变量，y为内层变量)

  -- 定义多项式 f = x² - y²
  -- x 表示为 B 中的变量 (Polynomial.X)
  -- y 表示为 A 中的变量，嵌入到 B 中作为常数多项式 (Polynomial.C (Polynomial.X : A))
  let x : B := Polynomial.X
  let y : B := Polynomial.C (Polynomial.X : A)
  let f : B := x^2 - y^2

  -- 构造由 f 生成的主理想
  let I : Ideal B := Ideal.span {f}

  -- 定义商环 R = B / I
  B ⧸ I
theorem problem (F : Type _) [Field F]
    ( a : quotientRing F ) (h1 : ∃ n : ℕ, a ^ n = 0) (h2 : a * a = a) : a = 0 := by
  sorry

I don't know why Lean4 is giving me an error:
failed to synthesize
HPow (quotientRing F) ℕ ?m.2033
Additional diagnostic information may be available using the set_option diagnostics true command.
I tried to construct the instance of that quotient ring but failed, and I don't understand why. :smiling_face_with_tear:

[Kenny Lau]

replace def with abbrev

[Kenny Lau]

def basically doesn't come with any typeclasses

[Kenny Lau]

you should also try to avoid anything with abbrev as well

[Kenny Lau]

basically, avoid defining types

[Kenny Lau]

substitute the whole definition of the type whenever you have to use it; if you think it's too long, the I can be a def without any problem, because I is not a type

[Kenny Lau]

so in problem, instead of quotientRing F, you should have Polynomial (Polynomial F)⧸ I

[Hbz]

I get it. You're really amazing. Would you mind if I become your disciple? :laughing:

[Kenny Lau]

well, if you ask questions here, someone will eventually answer

[Hbz]

:joy: