ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>P' : Type u_3<VAR>CommRing P'<VAR>Algebra R P'<VAR>g : P →ₐ[R] P'<VAR>I : Submodule R P<GOAL>IsFractional S I → IsFractional S (Submodule.map g.toLinearMap I)
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>P' : Type u_3<VAR>CommRing P'<VAR>Algebra R P'<VAR>g : P →ₐ[R] P'<VAR>I : FractionalIdeal S P<GOAL>↑(FractionalIdeal.map g I) = Submodule.map g.toLinearMap ↑I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>P' : Type u_3<VAR>CommRing P'<VAR>Algebra R P'<VAR>I : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<VAR>y : P'<GOAL>y ∈ FractionalIdeal.map g I ↔ ∃ x ∈ I, g x = y
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : FractionalIdeal S P<GOAL>FractionalIdeal.map (AlgHom.id R P) I = I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>P' : Type u_3<VAR>CommRing P'<VAR>Algebra R P'<VAR>P'' : Type u_4<VAR>CommRing P''<VAR>Algebra R P''<VAR>I : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<VAR>g' : P' →ₐ[R] P''<GOAL>FractionalIdeal.map (g'.comp g) I = FractionalIdeal.map g' (FractionalIdeal.map g I)
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>P' : Type u_3<VAR>CommRing P'<VAR>Algebra R P'<VAR>g : P →ₐ[R] P'<VAR>I : Ideal R<GOAL>FractionalIdeal.map g ↑I = ↑I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>P' : Type u_3<VAR>CommRing P'<VAR>Algebra R P'<VAR>g : P →ₐ[R] P'<GOAL>FractionalIdeal.map g 1 = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>P' : Type u_3<VAR>CommRing P'<VAR>Algebra R P'<VAR>g : P →ₐ[R] P'<GOAL>FractionalIdeal.map g 0 = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>P' : Type u_3<VAR>CommRing P'<VAR>Algebra R P'<VAR>I J : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<GOAL>FractionalIdeal.map g (I + J) = FractionalIdeal.map g I + FractionalIdeal.map g J
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>P' : Type u_3<VAR>CommRing P'<VAR>Algebra R P'<VAR>I J : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<GOAL>FractionalIdeal.map g (I * J) = FractionalIdeal.map g I * FractionalIdeal.map g J
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>P' : Type u_3<VAR>CommRing P'<VAR>Algebra R P'<VAR>I : FractionalIdeal S P<VAR>g : P ≃ₐ[R] P'<GOAL>FractionalIdeal.map (↑g.symm) (FractionalIdeal.map (↑g) I) = I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>P' : Type u_3<VAR>CommRing P'<VAR>Algebra R P'<VAR>I : FractionalIdeal S P'<VAR>g : P ≃ₐ[R] P'<GOAL>FractionalIdeal.map (↑g) (FractionalIdeal.map (↑g.symm) I) = I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>P' : Type u_3<VAR>CommRing P'<VAR>Algebra R P'<VAR>f : P →ₐ[R] P'<VAR>h : Function.Injective ⇑f<VAR>x : P<VAR>I : FractionalIdeal S P<GOAL>f x ∈ FractionalIdeal.map f I ↔ x ∈ I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>P' : Type u_3<VAR>CommRing P'<VAR>Algebra R P'<VAR>f : P →ₐ[R] P'<VAR>h : Function.Injective ⇑f<GOAL>Function.Injective (FractionalIdeal.map f)
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>P' : Type u_3<VAR>CommRing P'<VAR>Algebra R P'<VAR>g : P ≃ₐ[R] P'<GOAL>⇑(FractionalIdeal.mapEquiv g) = FractionalIdeal.map ↑g
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>P' : Type u_3<VAR>CommRing P'<VAR>Algebra R P'<VAR>g : P ≃ₐ[R] P'<VAR>I : FractionalIdeal S P<GOAL>(FractionalIdeal.mapEquiv g) I = FractionalIdeal.map (↑g) I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>P' : Type u_3<VAR>CommRing P'<VAR>Algebra R P'<VAR>g : P ≃ₐ[R] P'<GOAL>(FractionalIdeal.mapEquiv g).symm = FractionalIdeal.mapEquiv g.symm
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<GOAL>FractionalIdeal.mapEquiv AlgEquiv.refl = RingEquiv.refl (FractionalIdeal S P)
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>s : Set P<GOAL>IsFractional S (Submodule.span R s) ↔ ∃ a ∈ S, ∀ b ∈ s, IsLocalization.IsInteger R (a • b)
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>I : Submodule R P<VAR>hI : I.FG<GOAL>IsFractional S I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I J : FractionalIdeal S P<VAR>x : P<VAR>hx : x ∈ I * J<GOAL>∃ T T', ↑T ⊆ ↑I ∧ ↑T' ⊆ ↑J ∧ x ∈ Submodule.span R (↑T * ↑T')
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>inj : Function.Injective ⇑(algebraMap R P)<VAR>I : Ideal R<GOAL>(↑↑I).FG ↔ I.FG
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : (FractionalIdeal S P)ˣ<GOAL>(↑↑I).FG
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : FractionalIdeal S P<VAR>h : IsUnit I<GOAL>(↑I).FG
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>inj : Function.Injective ⇑(algebraMap R P)<VAR>I : Ideal R<VAR>h : IsUnit ↑I<GOAL>I.FG
<VAR>R : Type u_5<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_6<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_7<VAR>CommRing P'<VAR>Algebra R P'<VAR>loc' : IsLocalization S P'<GOAL>FractionalIdeal.canonicalEquiv S P P' = FractionalIdeal.mapEquiv (let __src := IsLocalization.ringEquivOfRingEquiv P P' (RingEquiv.refl R) ⋯; { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ })
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>CommRing P'<VAR>Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>I : FractionalIdeal S P<VAR>x : P'<GOAL>x ∈ (FractionalIdeal.canonicalEquiv S P P') I ↔ ∃ y ∈ I, (IsLocalization.map P' (RingHom.id R) ⋯) y = x
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>CommRing P'<VAR>Algebra R P'<VAR>loc' : IsLocalization S P'<GOAL>(FractionalIdeal.canonicalEquiv S P P').symm = FractionalIdeal.canonicalEquiv S P' P
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>CommRing P'<VAR>Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>I : FractionalIdeal S P'<GOAL>(FractionalIdeal.canonicalEquiv S P P') ((FractionalIdeal.canonicalEquiv S P' P) I) = I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>CommRing P'<VAR>Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_5<VAR>CommRing P''<VAR>Algebra R P''<VAR>IsLocalization S P''<VAR>I : FractionalIdeal S P<GOAL>(FractionalIdeal.canonicalEquiv S P' P'') ((FractionalIdeal.canonicalEquiv S P P') I) = (FractionalIdeal.canonicalEquiv S P P'') I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>CommRing P'<VAR>Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_5<VAR>CommRing P''<VAR>Algebra R P''<VAR>IsLocalization S P''<GOAL>(FractionalIdeal.canonicalEquiv S P P').trans (FractionalIdeal.canonicalEquiv S P' P'') = FractionalIdeal.canonicalEquiv S P P''
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>CommRing P'<VAR>Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>I : Ideal R<GOAL>(FractionalIdeal.canonicalEquiv S P P') ↑I = ↑I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<GOAL>FractionalIdeal.canonicalEquiv S P P = RingEquiv.refl (FractionalIdeal S P)
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_3<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>I : FractionalIdeal R⁰ K<VAR>Nontrivial R<VAR>hI : I ≠ 0<GOAL>∃ x, x ≠ 0 ∧ (algebraMap R K) x ∈ I
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_3<VAR>K' : Type u_4<VAR>Field K<VAR>Field K'<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>Algebra R K'<VAR>IsFractionRing R K'<VAR>I : FractionalIdeal R⁰ K<VAR>h : K →ₐ[R] K'<VAR>Nontrivial R<VAR>hI : I ≠ 0<GOAL>FractionalIdeal.map h I ≠ 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_3<VAR>K' : Type u_4<VAR>Field K<VAR>Field K'<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>Algebra R K'<VAR>IsFractionRing R K'<VAR>I : FractionalIdeal R⁰ K<VAR>h : K →ₐ[R] K'<VAR>Nontrivial R<GOAL>FractionalIdeal.map h I = 0 ↔ I = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_3<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<GOAL>Function.Injective fun I => ↑I
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_3<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>I J : Ideal R<GOAL>↑I = ↑J ↔ I = J
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_3<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>I : Ideal R<GOAL>↑I = 0 ↔ I = ⊥
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_3<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>I : Ideal R<GOAL>↑I ≠ 0 ↔ I ≠ ⊥
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_3<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>I : Ideal R<GOAL>↑I = 1 ↔ I = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_3<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>I : Ideal R<GOAL>↑I ≠ 1 ↔ I ≠ 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_3<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>Nontrivial R<VAR>I : FractionalIdeal R⁰ K<GOAL>I.num = 0 ↔ I = 0
<VAR>R₁ : Type u_3<VAR>CommRing R₁<VAR>K : Type u_4<VAR>Field K<VAR>Algebra R₁ K<VAR>I J : FractionalIdeal R₁⁰ K<VAR>h : I * J = 1<GOAL>I ≠ 0
<VAR>R₁ : Type u_3<VAR>CommRing R₁<VAR>K : Type u_4<VAR>Field K<VAR>Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>IsDomain R₁<VAR>I J : Submodule R₁ K<GOAL>IsFractional R₁⁰ I → IsFractional R₁⁰ J → J ≠ 0 → IsFractional R₁⁰ (I / J)
<VAR>R₁ : Type u_3<VAR>CommRing R₁<VAR>K : Type u_4<VAR>Field K<VAR>Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>IsDomain R₁<VAR>I J : FractionalIdeal R₁⁰ K<VAR>h : J ≠ 0<GOAL>IsFractional R₁⁰ (↑I / ↑J)
<VAR>R₁ : Type u_3<VAR>CommRing R₁<VAR>K : Type u_4<VAR>Field K<VAR>Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>IsDomain R₁<VAR>I : FractionalIdeal R₁⁰ K<GOAL>I / 0 = 0
<VAR>R₁ : Type u_3<VAR>CommRing R₁<VAR>K : Type u_4<VAR>Field K<VAR>Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>IsDomain R₁<VAR>I J : FractionalIdeal R₁⁰ K<VAR>h : J ≠ 0<GOAL>I / J = ⟨↑I / ↑J, ⋯⟩
<VAR>R₁ : Type u_3<VAR>CommRing R₁<VAR>K : Type u_4<VAR>Field K<VAR>Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>IsDomain R₁<VAR>I J : FractionalIdeal R₁⁰ K<VAR>hJ : J ≠ 0<GOAL>↑(I / J) = ↑I / ↑J
<VAR>R₁ : Type u_3<VAR>CommRing R₁<VAR>K : Type u_4<VAR>Field K<VAR>Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>IsDomain R₁<VAR>I J : FractionalIdeal R₁⁰ K<VAR>h : J ≠ 0<VAR>x : K<GOAL>x ∈ I / J ↔ ∀ y ∈ J, x * y ∈ I
<VAR>R₁ : Type u_3<VAR>CommRing R₁<VAR>K : Type u_4<VAR>Field K<VAR>Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>IsDomain R₁<VAR>I : FractionalIdeal R₁⁰ K<GOAL>I * (1 / I) ≤ 1
<VAR>R₁ : Type u_3<VAR>CommRing R₁<VAR>K : Type u_4<VAR>Field K<VAR>Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>IsDomain R₁<VAR>I : FractionalIdeal R₁⁰ K<VAR>hI : I ≤ 1<GOAL>I ≤ I * (1 / I)
<VAR>R₁ : Type u_3<VAR>CommRing R₁<VAR>K : Type u_4<VAR>Field K<VAR>Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>IsDomain R₁<VAR>I J J' : FractionalIdeal R₁⁰ K<VAR>hJ' : J' ≠ 0<GOAL>I ≤ J / J' ↔ ∀ x ∈ I, ∀ y ∈ J', x * y ∈ J
<VAR>R₁ : Type u_3<VAR>CommRing R₁<VAR>K : Type u_4<VAR>Field K<VAR>Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>IsDomain R₁<VAR>I J J' : FractionalIdeal R₁⁰ K<VAR>hJ' : J' ≠ 0<GOAL>I ≤ J / J' ↔ I * J' ≤ J
<VAR>R₁ : Type u_3<VAR>CommRing R₁<VAR>K : Type u_4<VAR>Field K<VAR>Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>IsDomain R₁<VAR>I : FractionalIdeal R₁⁰ K<GOAL>I / 1 = I
<VAR>R₁ : Type u_3<VAR>CommRing R₁<VAR>K : Type u_4<VAR>Field K<VAR>Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>IsDomain R₁<VAR>I J : FractionalIdeal R₁⁰ K<VAR>h : I * J = 1<GOAL>J = 1 / I
<VAR>R₁ : Type u_3<VAR>CommRing R₁<VAR>K : Type u_4<VAR>Field K<VAR>Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>IsDomain R₁<VAR>I : FractionalIdeal R₁⁰ K<GOAL>I * (1 / I) = 1 ↔ ∃ J, I * J = 1
<VAR>R₁ : Type u_3<VAR>CommRing R₁<VAR>K : Type u_4<VAR>Field K<VAR>Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>IsDomain R₁<VAR>K' : Type u_5<VAR>Field K'<VAR>Algebra R₁ K'<VAR>IsFractionRing R₁ K'<VAR>I J : FractionalIdeal R₁⁰ K<VAR>h : K ≃ₐ[R₁] K'<GOAL>FractionalIdeal.map (↑h) (I / J) = FractionalIdeal.map (↑h) I / FractionalIdeal.map (↑h) J
<VAR>R₁ : Type u_3<VAR>CommRing R₁<VAR>K : Type u_4<VAR>Field K<VAR>Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>IsDomain R₁<VAR>K' : Type u_5<VAR>Field K'<VAR>Algebra R₁ K'<VAR>IsFractionRing R₁ K'<VAR>I : FractionalIdeal R₁⁰ K<VAR>h : K ≃ₐ[R₁] K'<GOAL>FractionalIdeal.map (↑h) (1 / I) = 1 / FractionalIdeal.map (↑h) I
<VAR>K : Type u_4<VAR>L : Type u_5<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>IsFractionRing K L<VAR>I : FractionalIdeal K⁰ L<GOAL>I = 0 ∨ I = 1
<VAR>R₁ : Type u_3<VAR>K : Type u_4<VAR>CommRing R₁<VAR>Field K<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>hF : IsField R₁<VAR>I : FractionalIdeal R₁⁰ K<GOAL>I = 0 ∨ I = 1
<VAR>R₁ : Type u_3<VAR>CommRing R₁<VAR>K : Type u_4<VAR>Field K<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>ι : Type u_5<VAR>s : Finset ι<VAR>f : ι → K<GOAL>↑(FractionalIdeal.spanFinset R₁ s f) = Submodule.span R₁ (f '' ↑s)
<VAR>R₁ : Type u_3<VAR>CommRing R₁<VAR>K : Type u_4<VAR>Field K<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>ι : Type u_5<VAR>s : Finset ι<VAR>f : ι → K<GOAL>FractionalIdeal.spanFinset R₁ s f = 0 ↔ ∀ j ∈ s, f j = 0
<VAR>R₁ : Type u_3<VAR>CommRing R₁<VAR>K : Type u_4<VAR>Field K<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>ι : Type u_5<VAR>s : Finset ι<VAR>f : ι → K<GOAL>FractionalIdeal.spanFinset R₁ s f ≠ 0 ↔ ∃ j ∈ s, f j ≠ 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>x : P<GOAL>IsFractional S (Submodule.span R {x})
<VAR>R : Type u_5<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_6<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>x : P<GOAL>FractionalIdeal.spanSingleton S x = ⟨Submodule.span R {x}, ⋯⟩
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>x : P<GOAL>↑(FractionalIdeal.spanSingleton S x) = Submodule.span R {x}
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>x y : P<GOAL>x ∈ FractionalIdeal.spanSingleton S y ↔ ∃ z, z • y = x
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>x : P<GOAL>x ∈ FractionalIdeal.spanSingleton S x
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>I : FractionalIdeal S P<GOAL>FractionalIdeal.spanSingleton S ((algebraMap R P) ↑I.den) * I = ↑I.num
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>x : P<VAR>I : FractionalIdeal S P<GOAL>FractionalIdeal.spanSingleton S x ≤ I ↔ x ∈ I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>NoZeroSMulDivisors R P<VAR>x y : P<GOAL>FractionalIdeal.spanSingleton S x = FractionalIdeal.spanSingleton S y ↔ ∃ z, z • x = y
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>I : FractionalIdeal S P<VAR>(↑I).IsPrincipal<GOAL>I = FractionalIdeal.spanSingleton S (Submodule.IsPrincipal.generator ↑I)
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>I : FractionalIdeal S P<GOAL>(↑I).IsPrincipal ↔ ∃ x, I = FractionalIdeal.spanSingleton S x
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<GOAL>FractionalIdeal.spanSingleton S 0 = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>y : P<GOAL>FractionalIdeal.spanSingleton S y = 0 ↔ y = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>y : P<GOAL>FractionalIdeal.spanSingleton S y ≠ 0 ↔ y ≠ 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<GOAL>FractionalIdeal.spanSingleton S 1 = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>x y : P<GOAL>FractionalIdeal.spanSingleton S x * FractionalIdeal.spanSingleton S y = FractionalIdeal.spanSingleton S (x * y)
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>x : P<VAR>n : ℕ<GOAL>FractionalIdeal.spanSingleton S x ^ n = FractionalIdeal.spanSingleton S (x ^ n)
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>x : R<GOAL>↑(Ideal.span {x}) = FractionalIdeal.spanSingleton S ((algebraMap R P) x)
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_5<VAR>CommRing P'<VAR>Algebra R P'<VAR>IsLocalization S P'<VAR>x : P<GOAL>(FractionalIdeal.canonicalEquiv S P P') (FractionalIdeal.spanSingleton S x) = FractionalIdeal.spanSingleton S ((IsLocalization.map P' (RingHom.id R) ⋯) x)
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>x y : P<VAR>I : FractionalIdeal S P<GOAL>y ∈ FractionalIdeal.spanSingleton S x * I ↔ ∃ y' ∈ I, y = x * y'
<VAR>R₁ : Type u_3<VAR>CommRing R₁<VAR>K : Type u_4<VAR>Field K<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>I J : Ideal R₁<VAR>x y : R₁<VAR>hy : y ∈ R₁⁰<GOAL>FractionalIdeal.spanSingleton R₁⁰ (IsLocalization.mk' K x ⟨y, hy⟩) * ↑I = ↑J ↔ Ideal.span {x} * I = Ideal.span {y} * J
<VAR>R₁ : Type u_3<VAR>CommRing R₁<VAR>K : Type u_4<VAR>Field K<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>I J : Ideal R₁<VAR>z : K<GOAL>FractionalIdeal.spanSingleton R₁⁰ z * ↑I = ↑J ↔ Ideal.span {(IsLocalization.sec R₁⁰ z).1} * I = Ideal.span {↑(IsLocalization.sec R₁⁰ z).2} * J
<VAR>R₁ : Type u_3<VAR>CommRing R₁<VAR>K : Type u_4<VAR>Field K<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>IsDomain R₁<VAR>x : K<GOAL>1 / FractionalIdeal.spanSingleton R₁⁰ x = FractionalIdeal.spanSingleton R₁⁰ x⁻¹
<VAR>R₁ : Type u_3<VAR>CommRing R₁<VAR>K : Type u_4<VAR>Field K<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>IsDomain R₁<VAR>J : FractionalIdeal R₁⁰ K<VAR>d : K<GOAL>J / FractionalIdeal.spanSingleton R₁⁰ d = FractionalIdeal.spanSingleton R₁⁰ d⁻¹ * J
<VAR>R₁ : Type u_3<VAR>CommRing R₁<VAR>K : Type u_4<VAR>Field K<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>IsDomain R₁<VAR>I : FractionalIdeal R₁⁰ K<GOAL>∃ a aI, a ≠ 0 ∧ I = FractionalIdeal.spanSingleton R₁⁰ ((algebraMap R₁ K) a)⁻¹ * ↑aI
<VAR>R : Type u_6<VAR>CommRing R<VAR>K : Type u_5<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>haJ : I = FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<GOAL>J ≠ 0
<VAR>R : Type u_6<VAR>CommRing R<VAR>K : Type u_5<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>haJ : I = FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<GOAL>Ideal.span {a} ≠ 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>x : P<VAR>I J : FractionalIdeal S P<GOAL>I ≤ FractionalIdeal.spanSingleton S x * J ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>x : P<VAR>I J : FractionalIdeal S P<GOAL>FractionalIdeal.spanSingleton S x * I ≤ J ↔ ∀ z ∈ I, x * z ∈ J
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>x : P<VAR>I J : FractionalIdeal S P<GOAL>I = FractionalIdeal.spanSingleton S x * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI) ∧ ∀ z ∈ J, x * z ∈ I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>I : FractionalIdeal S P<GOAL>↑I.num ≤ I
<VAR>R₁ : Type u_3<VAR>CommRing R₁<VAR>K : Type u_4<VAR>Field K<VAR>Algebra R₁ K<GOAL>IsNoetherian R₁ ↥↑0
<VAR>R₁ : Type u_3<VAR>CommRing R₁<VAR>K : Type u_4<VAR>Field K<VAR>Algebra R₁ K<VAR>I : FractionalIdeal R₁⁰ K<GOAL>IsNoetherian R₁ ↥↑I ↔ ∀ J ≤ I, (↑J).FG
<VAR>R₁ : Type u_3<VAR>CommRing R₁<VAR>K : Type u_4<VAR>Field K<VAR>Algebra R₁ K<VAR>IsNoetherianRing R₁<VAR>I : Ideal R₁<GOAL>IsNoetherian R₁ ↥↑↑I
<VAR>R₁ : Type u_3<VAR>CommRing R₁<VAR>K : Type u_4<VAR>Field K<VAR>Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>IsDomain R₁<VAR>x : R₁<VAR>I : FractionalIdeal R₁⁰ K<VAR>hI : IsNoetherian R₁ ↥↑I<GOAL>IsNoetherian R₁ ↥↑(FractionalIdeal.spanSingleton R₁⁰ ((algebraMap R₁ K) x)⁻¹ * I)
<VAR>R₁ : Type u_3<VAR>CommRing R₁<VAR>K : Type u_4<VAR>Field K<VAR>Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>IsDomain R₁<VAR>IsNoetherianRing R₁<VAR>I : FractionalIdeal R₁⁰ K<GOAL>IsNoetherian R₁ ↥↑I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>x : P<VAR>hx : IsIntegral R x<GOAL>IsFractional S (Subalgebra.toSubmodule (Algebra.adjoin R {x}))
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>x : P<VAR>hx : IsIntegral R x<GOAL>↑(FractionalIdeal.adjoinIntegral S x hx) = Subalgebra.toSubmodule (Algebra.adjoin R {x})
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>x : P<VAR>hx : IsIntegral R x<GOAL>x ∈ FractionalIdeal.adjoinIntegral S x hx
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>CommRing Rₘ<VAR>Algebra R Rₘ<VAR>CommRing Sₘ<VAR>Algebra S Sₘ<VAR>M : Submonoid R<VAR>IsLocalization M Rₘ<VAR>IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>Algebra Rₘ Sₘ<VAR>Algebra R Sₘ<VAR>IsScalarTower R Rₘ Sₘ<VAR>IsScalarTower R S Sₘ<VAR>ι : Type u_5<VAR>Fintype ι<VAR>DecidableEq ι<VAR>b : Basis ι R S<VAR>a : S<GOAL>(algebraMap R Rₘ).mapMatrix ((Algebra.leftMulMatrix b) a) = (Algebra.leftMulMatrix (Basis.localizationLocalization Rₘ M Sₘ b)) ((algebraMap S Sₘ) a)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>CommRing Rₘ<VAR>Algebra R Rₘ<VAR>CommRing Sₘ<VAR>Algebra S Sₘ<VAR>M : Submonoid R<VAR>IsLocalization M Rₘ<VAR>IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>Algebra Rₘ Sₘ<VAR>Algebra R Sₘ<VAR>IsScalarTower R Rₘ Sₘ<VAR>IsScalarTower R S Sₘ<VAR>Module.Free R S<VAR>Module.Finite R S<VAR>a : S<GOAL>(Algebra.norm Rₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((Algebra.norm R) a)