FractionRing

Stream: new members

[亚历山大大帝]

Why can't inferInstance in “haveI : Algebra R (MvPolynomial X R) := inferInstance. haveI : IsDomain (MvPolynomial X R) := inferInstance” succeed?

Lean4WebDownload (1).lean

[Ilmārs Cīrulis]

(deleted)

[Ruben Van de Velde]

Again, read #mwe and #backticks so we can help you

[Junyan Xu]

CommSemiring and Algebra are data and you need to use letI

Why are you declaring instances that can already be found by inferInstance?

[亚历山大大帝]

IsLocalization.of_le can it be used in this environment? What other types need to be instantiated?
Lean4WebDownload (2).lean

import Mathlib


open IsFractionRing
-- 声明变量
variable {u v : Type} {R : Type u} {X : Type v} [CommRing R] [IsDomain R]
variable {S : Type v} [CommSemiring S] [Algebra R S]
variable (M : Submonoid R) [IsLocalization M S] (N : Submonoid R)

theorem FractionRing.isField :
    IsField (FractionRing (MvPolynomial X R)) := by
  -- 使用 letI 显式声明必要实例，确保类型类解析器能找到它们
  letI : CommSemiring (MvPolynomial X R) := inferInstance
  letI : Algebra R (MvPolynomial X R) := inferInstance
  letI : IsDomain (MvPolynomial X R) := inferInstance
  -- 构造 IsFractionRing 实例
  letI isFractionRingInstance : IsFractionRing (MvPolynomial X R) (FractionRing (MvPolynomial X R)) := by
    apply IsLocalization.of_le (MvPolynomial X R) (nonZeroDivisors (MvPolynomial X R)) (nonZeroDivisors (MvPolynomial X R))
    <;> simp [nonZeroDivisors]
    <;> exact fun r hr => by
      simp [nonZeroDivisors, hr]
    <;> exact inferInstance
  -- 应用定理证明分式环是域
  exact IsFractionRing.toField (MvPolynomial X R)
  <;> infer_instance
example {R : Type u} [CommRing R] [IsDomain R] (I : Type v) :
    FractionRing (MvPolynomial I R) ≃ₐ[R] FractionRing (MvPolynomial I (FractionRing R)) := by
  -- 构造代数同构
  refine' AlgEquiv.symm _
  -- 应用分式域的代数同构定理
  exact IsLocalization.algEquiv (nonZeroDivisors (MvPolynomial I R)) (le_refl _) (FractionRing (MvPolynomial I R)) (FractionRing (MvPolynomial I (FractionRing R)))
  <;> infer_instance