ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>CommRing A<VAR>Field K<VAR>CommRing B<VAR>Field L<VAR>Algebra A K<VAR>Algebra B L<VAR>Algebra A B<VAR>Algebra K L<VAR>Algebra A L<VAR>IsScalarTower A K L<VAR>IsScalarTower A B L<VAR>IsDomain A<VAR>IsFractionRing A K<VAR>IsIntegralClosure B A L<VAR>IsFractionRing B L<VAR>FiniteDimensional K L<VAR>Algebra.IsSeparable K L<VAR>IsIntegrallyClosed A<VAR>IsDedekindDomain B<VAR>NoZeroSMulDivisors A B<GOAL>↑(differentIdeal A B) = (FractionalIdeal.dual A K 1)⁻¹
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>CommRing A<VAR>Field K<VAR>CommRing B<VAR>Field L<VAR>Algebra A K<VAR>Algebra B L<VAR>Algebra A B<VAR>Algebra K L<VAR>Algebra A L<VAR>IsScalarTower A K L<VAR>IsScalarTower A B L<VAR>IsDomain A<VAR>IsFractionRing A K<VAR>IsIntegralClosure B A L<VAR>IsFractionRing B L<VAR>FiniteDimensional K L<VAR>Algebra.IsSeparable K L<VAR>IsIntegrallyClosed A<VAR>IsDedekindDomain B<VAR>I : FractionalIdeal B⁰ L<VAR>hI : I ≠ 0<VAR>NoZeroSMulDivisors A B<GOAL>↑(differentIdeal A B) ≤ I ↔ Submodule.map (↑A (Algebra.trace K L)) (Submodule.restrictScalars A ↑I⁻¹) ≤ 1
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>CommRing A<VAR>Field K<VAR>CommRing B<VAR>Field L<VAR>Algebra A K<VAR>Algebra B L<VAR>Algebra A B<VAR>Algebra K L<VAR>Algebra A L<VAR>IsScalarTower A K L<VAR>IsScalarTower A B L<VAR>IsDomain A<VAR>IsFractionRing A K<VAR>IsIntegralClosure B A L<VAR>IsFractionRing B L<VAR>FiniteDimensional K L<VAR>Algebra.IsSeparable K L<VAR>IsIntegrallyClosed A<VAR>IsDedekindDomain B<VAR>I : Ideal B<VAR>hI : I ≠ ⊥<VAR>NoZeroSMulDivisors A B<GOAL>differentIdeal A B ≤ I ↔ Submodule.map (↑A (Algebra.trace K L)) (Submodule.restrictScalars A ↑(↑I)⁻¹) ≤ 1
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>CommRing A<VAR>Field K<VAR>Field L<VAR>Algebra A K<VAR>Algebra K L<VAR>Algebra A L<VAR>IsScalarTower A K L<VAR>IsDomain A<VAR>IsFractionRing A K<VAR>FiniteDimensional K L<VAR>Algebra.IsSeparable K L<VAR>IsIntegrallyClosed A<VAR>x : L<VAR>hx : Algebra.adjoin K {x} = ⊤<VAR>hAx : IsIntegral A x<GOAL>(Algebra.traceForm K L).dualSubmodule (Subalgebra.toSubmodule (Algebra.adjoin A {x})) = ((Polynomial.aeval x) (Polynomial.derivative (minpoly K x)))⁻¹ • Subalgebra.toSubmodule (Algebra.adjoin A {x})
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>CommRing A<VAR>Field K<VAR>CommRing B<VAR>Field L<VAR>Algebra A K<VAR>Algebra B L<VAR>Algebra A B<VAR>Algebra K L<VAR>Algebra A L<VAR>IsScalarTower A K L<VAR>IsScalarTower A B L<VAR>IsDomain A<VAR>IsFractionRing A K<VAR>IsIntegralClosure B A L<VAR>FiniteDimensional K L<VAR>Algebra.IsSeparable K L<VAR>IsIntegrallyClosed A<VAR>IsDedekindDomain B<VAR>NoZeroSMulDivisors A B<VAR>x : B<VAR>hx : Algebra.adjoin K {(algebraMap B L) x} = ⊤<GOAL>conductor A x * differentIdeal A B = Ideal.span {(Polynomial.aeval x) (Polynomial.derivative (minpoly A x))}
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>CommRing A<VAR>Field K<VAR>CommRing B<VAR>Field L<VAR>Algebra A K<VAR>Algebra B L<VAR>Algebra A B<VAR>Algebra K L<VAR>Algebra A L<VAR>IsScalarTower A K L<VAR>IsScalarTower A B L<VAR>IsDomain A<VAR>IsFractionRing A K<VAR>IsIntegralClosure B A L<VAR>FiniteDimensional K L<VAR>Algebra.IsSeparable K L<VAR>IsIntegrallyClosed A<VAR>IsDedekindDomain B<VAR>NoZeroSMulDivisors A B<VAR>x : B<VAR>hx : Algebra.adjoin K {(algebraMap B L) x} = ⊤<GOAL>(Polynomial.aeval x) (Polynomial.derivative (minpoly A x)) ∈ differentIdeal A B
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>DecidableEq l<VAR>CommRing R<GOAL>(Matrix.J l R)ᵀ = -Matrix.J l R
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>DecidableEq l<VAR>CommRing R<VAR>Fintype l<GOAL>Matrix.J l R * Matrix.J l R = -1
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>DecidableEq l<VAR>CommRing R<VAR>Fintype l<GOAL>(Matrix.J l R)⁻¹ = -Matrix.J l R
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>DecidableEq l<VAR>CommRing R<VAR>Fintype l<GOAL>(Matrix.J l R).det * (Matrix.J l R).det = 1
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>DecidableEq l<VAR>CommRing R<VAR>Fintype l<GOAL>IsUnit (Matrix.J l R).det
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>DecidableEq l<VAR>Fintype l<VAR>CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<GOAL>A ∈ Matrix.symplecticGroup l R ↔ A * Matrix.J l R * Aᵀ = Matrix.J l R
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>DecidableEq l<VAR>Fintype l<VAR>CommRing R<GOAL>Matrix.J l R ∈ Matrix.symplecticGroup l R
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>DecidableEq l<VAR>Fintype l<VAR>CommRing R<GOAL>↑(SymplecticGroup.symJ l R) = Matrix.J l R
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>DecidableEq l<VAR>Fintype l<VAR>CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<VAR>h : A ∈ Matrix.symplecticGroup l R<GOAL>-A ∈ Matrix.symplecticGroup l R
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>DecidableEq l<VAR>Fintype l<VAR>CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<VAR>hA : A ∈ Matrix.symplecticGroup l R<GOAL>IsUnit A.det
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>DecidableEq l<VAR>Fintype l<VAR>CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<VAR>hA : A ∈ Matrix.symplecticGroup l R<GOAL>Aᵀ ∈ Matrix.symplecticGroup l R
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>DecidableEq l<VAR>Fintype l<VAR>CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<GOAL>Aᵀ ∈ Matrix.symplecticGroup l R ↔ A ∈ Matrix.symplecticGroup l R
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>DecidableEq l<VAR>Fintype l<VAR>CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<GOAL>A ∈ Matrix.symplecticGroup l R ↔ Aᵀ * Matrix.J l R * A = Matrix.J l R
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>DecidableEq l<VAR>Fintype l<VAR>CommRing R<VAR>A : ↥(Matrix.symplecticGroup l R)<GOAL>↑A⁻¹ = -Matrix.J l R * (↑A)ᵀ * Matrix.J l R
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>DecidableEq l<VAR>Fintype l<VAR>CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<VAR>hA : A ∈ Matrix.symplecticGroup l R<GOAL>-(Matrix.J l R * Aᵀ * Matrix.J l R * A) = 1
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>DecidableEq l<VAR>Fintype l<VAR>CommRing R<VAR>A : ↥(Matrix.symplecticGroup l R)<GOAL>↑A⁻¹ = (↑A)⁻¹
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>DecidableEq l<VAR>Fintype l<VAR>CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<VAR>hA : A ∈ Matrix.symplecticGroup l R<GOAL>A⁻¹ = -Matrix.J l R * Aᵀ * Matrix.J l R
<VAR>K : Type u_3<VAR>Field K<VAR>R₁ : Type u_4<VAR>CommRing R₁<VAR>IsDomain R₁<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>I : FractionalIdeal R₁⁰ K<GOAL>I⁻¹ = 1 / I
<VAR>K : Type u_3<VAR>Field K<VAR>R₁ : Type u_4<VAR>CommRing R₁<VAR>IsDomain R₁<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<GOAL>0⁻¹ = 0
<VAR>K : Type u_3<VAR>Field K<VAR>R₁ : Type u_4<VAR>CommRing R₁<VAR>IsDomain R₁<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>J : FractionalIdeal R₁⁰ K<VAR>h : J ≠ 0<GOAL>J⁻¹ = ⟨↑1 / ↑J, ⋯⟩
<VAR>K : Type u_3<VAR>Field K<VAR>R₁ : Type u_4<VAR>CommRing R₁<VAR>IsDomain R₁<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>J : FractionalIdeal R₁⁰ K<VAR>h : J ≠ 0<GOAL>↑J⁻¹ = IsLocalization.coeSubmodule K ⊤ / ↑J
<VAR>K : Type u_3<VAR>Field K<VAR>R₁ : Type u_4<VAR>CommRing R₁<VAR>IsDomain R₁<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>I : FractionalIdeal R₁⁰ K<VAR>hI : I ≠ 0<VAR>x : K<GOAL>x ∈ I⁻¹ ↔ ∀ y ∈ I, x * y ∈ 1
<VAR>K : Type u_3<VAR>Field K<VAR>R₁ : Type u_4<VAR>CommRing R₁<VAR>IsDomain R₁<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>I J : FractionalIdeal R₁⁰ K<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<VAR>hIJ : I ≤ J<GOAL>J⁻¹ ≤ I⁻¹
<VAR>K : Type u_3<VAR>Field K<VAR>R₁ : Type u_4<VAR>CommRing R₁<VAR>IsDomain R₁<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>I : FractionalIdeal R₁⁰ K<VAR>hI : I ≤ 1<GOAL>I ≤ I * I⁻¹
<VAR>K : Type u_3<VAR>Field K<VAR>R₁ : Type u_4<VAR>CommRing R₁<VAR>IsDomain R₁<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>I : Ideal R₁<GOAL>↑I ≤ ↑I * (↑I)⁻¹
<VAR>K : Type u_3<VAR>Field K<VAR>R₁ : Type u_4<VAR>CommRing R₁<VAR>IsDomain R₁<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>I J : FractionalIdeal R₁⁰ K<VAR>h : I * J = 1<GOAL>J = I⁻¹
<VAR>K : Type u_3<VAR>Field K<VAR>R₁ : Type u_4<VAR>CommRing R₁<VAR>IsDomain R₁<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>I : FractionalIdeal R₁⁰ K<GOAL>I * I⁻¹ = 1 ↔ ∃ J, I * J = 1
<VAR>K : Type u_3<VAR>Field K<VAR>R₁ : Type u_4<VAR>CommRing R₁<VAR>IsDomain R₁<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>I : FractionalIdeal R₁⁰ K<GOAL>I * I⁻¹ = 1 ↔ IsUnit I
<VAR>K : Type u_3<VAR>Field K<VAR>R₁ : Type u_4<VAR>CommRing R₁<VAR>IsDomain R₁<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<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) I⁻¹ = (FractionalIdeal.map (↑h) I)⁻¹
<VAR>K : Type u_3<VAR>Field K<VAR>R₁ : Type u_4<VAR>CommRing R₁<VAR>IsDomain R₁<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>x : K<GOAL>(FractionalIdeal.spanSingleton R₁⁰ x)⁻¹ = FractionalIdeal.spanSingleton R₁⁰ x⁻¹
<VAR>K : Type u_3<VAR>Field K<VAR>R₁ : Type u_4<VAR>CommRing R₁<VAR>IsDomain R₁<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>x y : K<GOAL>FractionalIdeal.spanSingleton R₁⁰ x / FractionalIdeal.spanSingleton R₁⁰ y = FractionalIdeal.spanSingleton R₁⁰ (x / y)
<VAR>K : Type u_3<VAR>Field K<VAR>R₁ : Type u_4<VAR>CommRing R₁<VAR>IsDomain R₁<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>x : K<VAR>hx : x ≠ 0<GOAL>FractionalIdeal.spanSingleton R₁⁰ x / FractionalIdeal.spanSingleton R₁⁰ x = 1
<VAR>K : Type u_3<VAR>Field K<VAR>R₁ : Type u_4<VAR>CommRing R₁<VAR>IsDomain R₁<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>x : R₁<VAR>hx : x ≠ 0<GOAL>↑(Ideal.span {x}) / ↑(Ideal.span {x}) = 1
<VAR>K : Type u_3<VAR>Field K<VAR>R₁ : Type u_4<VAR>CommRing R₁<VAR>IsDomain R₁<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>x : K<VAR>hx : x ≠ 0<GOAL>FractionalIdeal.spanSingleton R₁⁰ x * (FractionalIdeal.spanSingleton R₁⁰ x)⁻¹ = 1
<VAR>K : Type u_3<VAR>Field K<VAR>R₁ : Type u_4<VAR>CommRing R₁<VAR>IsDomain R₁<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>x : R₁<VAR>hx : x ≠ 0<GOAL>↑(Ideal.span {x}) * (↑(Ideal.span {x}))⁻¹ = 1
<VAR>K : Type u_3<VAR>Field K<VAR>R₁ : Type u_4<VAR>CommRing R₁<VAR>IsDomain R₁<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>x : K<VAR>hx : x ≠ 0<GOAL>(FractionalIdeal.spanSingleton R₁⁰ x)⁻¹ * FractionalIdeal.spanSingleton R₁⁰ x = 1
<VAR>K : Type u_3<VAR>Field K<VAR>R₁ : Type u_4<VAR>CommRing R₁<VAR>IsDomain R₁<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>x : R₁<VAR>hx : x ≠ 0<GOAL>(↑(Ideal.span {x}))⁻¹ * ↑(Ideal.span {x}) = 1
<VAR>K : Type u_3<VAR>Field K<VAR>R₁ : Type u_6<VAR>CommRing R₁<VAR>Algebra R₁ K<VAR>IsLocalization R₁⁰ K<VAR>I : FractionalIdeal R₁⁰ K<VAR>(↑I).IsPrincipal<VAR>h : I ≠ 0<GOAL>I * FractionalIdeal.spanSingleton R₁⁰ (Submodule.IsPrincipal.generator ↑I)⁻¹ = 1
<VAR>K : Type u_3<VAR>Field K<VAR>R₁ : Type u_4<VAR>CommRing R₁<VAR>IsDomain R₁<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>I : FractionalIdeal R₁⁰ K<VAR>(↑I).IsPrincipal<VAR>h : I ≠ 0<GOAL>I * I⁻¹ = 1
<VAR>K : Type u_3<VAR>Field K<VAR>R₁ : Type u_4<VAR>CommRing R₁<VAR>IsDomain R₁<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>I : FractionalIdeal R₁⁰ K<VAR>(↑I).IsPrincipal<GOAL>I * I⁻¹ = 1 ↔ Submodule.IsPrincipal.generator ↑I ≠ 0
<VAR>K : Type u_3<VAR>Field K<VAR>R₁ : Type u_4<VAR>CommRing R₁<VAR>IsDomain R₁<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>I : FractionalIdeal R₁⁰ K<VAR>(↑I).IsPrincipal<VAR>h : I ≠ 0<GOAL>(↑I⁻¹).IsPrincipal
<VAR>K : Type u_3<VAR>Field K<VAR>R₁ : Type u_4<VAR>CommRing R₁<VAR>IsDomain R₁<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>I : FractionalIdeal R₁⁰ K<VAR>hI : I ≠ ⊥<GOAL>(algebraMap R₁ K) ↑I.den ∈ I⁻¹
<VAR>K : Type u_3<VAR>Field K<VAR>R₁ : Type u_4<VAR>CommRing R₁<VAR>IsDomain R₁<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>I : FractionalIdeal R₁⁰ K<GOAL>↑I.num ≤ I * I⁻¹
<VAR>K : Type u_3<VAR>Field K<VAR>R₁ : Type u_4<VAR>CommRing R₁<VAR>IsDomain R₁<VAR>Algebra R₁ K<VAR>IsFractionRing R₁ K<VAR>I : FractionalIdeal R₁⁰ K<VAR>hI : I ≠ ⊥<GOAL>⊥ < I * I⁻¹
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>IsDomain A<VAR>Algebra A K<VAR>IsFractionRing A K<GOAL>IsDedekindDomainInv A ↔ ∀ (I : FractionalIdeal A⁰ K), I ≠ ⊥ → I * I⁻¹ = 1
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>IsDomain A<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>x : K<VAR>hx : IsIntegral A x<VAR>hI : IsUnit (FractionalIdeal.adjoinIntegral A⁰ x hx)<GOAL>FractionalIdeal.adjoinIntegral A⁰ x hx = 1
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>IsDomain A<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>h : IsDedekindDomainInv A<VAR>I : FractionalIdeal A⁰ K<VAR>hI : I ≠ 0<GOAL>I * I⁻¹ = 1
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>IsDomain A<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>h : IsDedekindDomainInv A<VAR>I : FractionalIdeal A⁰ K<VAR>hI : I ≠ 0<GOAL>I⁻¹ * I = 1
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>IsDomain A<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>h : IsDedekindDomainInv A<VAR>I : FractionalIdeal A⁰ K<VAR>hI : I ≠ 0<GOAL>IsUnit I
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDomain A<VAR>h : IsDedekindDomainInv A<GOAL>IsNoetherianRing A
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDomain A<VAR>h : IsDedekindDomainInv A<GOAL>IsIntegrallyClosed A
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDomain A<VAR>h : IsDedekindDomainInv A<GOAL>Ring.DimensionLEOne A
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDomain A<VAR>h : IsDedekindDomainInv A<GOAL>IsDedekindDomain A
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>IsDomain A<VAR>I : Ideal A<VAR>hI : I ≠ ⊥<GOAL>1 ∈ (↑I)⁻¹
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDedekindDomain A<VAR>hNF : ¬IsField A<VAR>I M : Ideal A<VAR>hI0 : I ≠ ⊥<VAR>hIM : I ≤ M<VAR>hM : M.IsMaximal<GOAL>∃ Z, (M ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I ∧ ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>IsDedekindDomain A<VAR>I : Ideal A<VAR>hI0 : I ≠ ⊥<VAR>hI1 : I ≠ ⊤<GOAL>¬(↑I)⁻¹ ≤ 1
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>IsDedekindDomain A<VAR>I : Ideal A<VAR>hI0 : I ≠ ⊥<VAR>hI1 : I ≠ ⊤<GOAL>∃ x ∈ (↑I)⁻¹, x ∉ 1
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>h : IsDedekindDomain A<VAR>I : Ideal A<VAR>hI0 : I ≠ ⊥<VAR>hI : (↑I * (↑I)⁻¹)⁻¹ ≤ 1<GOAL>↑I * (↑I)⁻¹ = 1
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>h : IsDedekindDomain A<VAR>I : Ideal A<VAR>hI0 : I ≠ ⊥<GOAL>↑I * (↑I)⁻¹ = 1
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>IsDedekindDomain A<VAR>I : FractionalIdeal A⁰ K<VAR>hne : I ≠ 0<GOAL>I * I⁻¹ = 1
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>IsDedekindDomain A<VAR>J : FractionalIdeal A⁰ K<VAR>hJ : J ≠ 0<VAR>I I' : FractionalIdeal A⁰ K<GOAL>I * J ≤ I' * J ↔ I ≤ I'
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>IsDedekindDomain A<VAR>J : FractionalIdeal A⁰ K<VAR>hJ : J ≠ 0<VAR>I I' : FractionalIdeal A⁰ K<GOAL>J * I ≤ J * I' ↔ I ≤ I'
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>IsDedekindDomain A<VAR>I : FractionalIdeal A⁰ K<VAR>hI : I ≠ 0<GOAL>StrictMono fun x => x * I
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>IsDedekindDomain A<VAR>I : FractionalIdeal A⁰ K<VAR>hI : I ≠ 0<GOAL>StrictMono fun x => I * x
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>IsDedekindDomain A<VAR>I J : FractionalIdeal A⁰ K<GOAL>I / J = I * J⁻¹
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDomain A<GOAL>IsDedekindDomain A ↔ IsDedekindDomainInv A
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDedekindDomain A<VAR>I J : Ideal A<GOAL>I ∣ J ↔ J ≤ I
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDedekindDomain A<VAR>I J : Ideal A<GOAL>DvdNotUnit I J ↔ J < I
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDedekindDomain A<VAR>I : Ideal A<VAR>x : A<GOAL>I ∣ Ideal.span {x} ↔ x ∈ I
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDedekindDomain A<VAR>P : Ideal A<VAR>h : Prime P<GOAL>P.IsPrime
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDedekindDomain A<VAR>P : Ideal A<VAR>hP : P ≠ ⊥<VAR>h : P.IsPrime<GOAL>Prime P
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDedekindDomain A<VAR>P : Ideal A<VAR>hP : P ≠ ⊥<GOAL>Prime P ↔ P.IsPrime
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDedekindDomain A<VAR>P : Ideal A<GOAL>P.IsPrime ↔ P = ⊥ ∨ Prime P
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDedekindDomain A<VAR>a : A<GOAL>Prime (Ideal.span {a}) ↔ Prime a
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDedekindDomain A<VAR>P : Ideal A<VAR>h : Prime P<VAR>Submodule.IsPrincipal P<GOAL>Prime (Submodule.IsPrincipal.generator P)
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDedekindDomain A<VAR>p I : Ideal A<VAR>hI : I ≠ ⊥<GOAL>p ∈ UniqueFactorizationMonoid.normalizedFactors I ↔ p.IsPrime ∧ I ≤ p
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDedekindDomain A<VAR>I : Ideal A<VAR>hI0 : I ≠ ⊥<VAR>hI1 : I ≠ ⊤<GOAL>StrictAnti fun x => I ^ x
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDedekindDomain A<VAR>I : Ideal A<VAR>hI0 : I ≠ ⊥<VAR>hI1 : I ≠ ⊤<VAR>e : ℕ<VAR>he : 2 ≤ e<GOAL>I ^ e < I
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDedekindDomain A<VAR>I : Ideal A<VAR>hI0 : I ≠ ⊥<VAR>hI1 : I ≠ ⊤<VAR>e : ℕ<GOAL>∃ x ∈ I ^ e, x ∉ I ^ (e + 1)
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDedekindDomain A<VAR>P I : Ideal A<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>i : ℕ<VAR>hlt : P ^ (i + 1) < I<VAR>hle : I ≤ P ^ i<GOAL>I = P ^ i
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDedekindDomain A<VAR>P : Ideal A<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>i : ℕ<GOAL>P ^ (i + 1) < P ^ i
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDedekindDomain A<VAR>x : A<VAR>n : ℕ<VAR>I : Ideal A<GOAL>Associates.mk I ^ n ≤ Associates.mk (Ideal.span {x}) ↔ x ∈ I ^ n
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>IsDedekindDomain A<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>I J : FractionalIdeal A⁰ K<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<GOAL>I ≤ J⁻¹ ↔ J ≤ I⁻¹
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>IsDedekindDomain A<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>I J : FractionalIdeal A⁰ K<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<GOAL>I⁻¹ ≤ J ↔ J⁻¹ ≤ I
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>IsDedekindDomain A<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>J : Ideal A<VAR>hJ : J ≠ ⊤<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>f : ι → K<VAR>j : ι<VAR>hjs : j ∈ s<VAR>hjf : f j ≠ 0<GOAL>∃ a, (∀ i ∈ s, IsLocalization.IsInteger A (a * f i)) ∧ ∃ i ∈ s, a * f i ∉ ↑J
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDedekindDomain A<VAR>I J : Ideal A<GOAL>(I ⊔ J) * (I ⊓ J) = I * J
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDedekindDomain A<VAR>I J : Ideal A<GOAL>gcd I J = I ⊔ J
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDedekindDomain A<VAR>I J : Ideal A<GOAL>lcm I J = I ⊓ J
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDedekindDomain A<VAR>I J : Ideal A<GOAL>IsCoprime I J ↔ gcd I J = 1
<VAR>K : Type u_3<VAR>Field K<VAR>p : K[X]<GOAL>UniqueFactorizationMonoid.factors (Ideal.span {p}) = Multiset.map (fun q => Ideal.span {q}) (UniqueFactorizationMonoid.factors p)
<VAR>T : Type u_4<VAR>CommRing T<VAR>IsDedekindDomain T<VAR>I : Ideal T<VAR>hI : I ≠ ⊥<GOAL>(UniqueFactorizationMonoid.normalizedFactors I).prod = I
<VAR>T : Type u_4<VAR>CommRing T<VAR>IsDedekindDomain T<VAR>I J : Ideal T<VAR>h : I ≤ J<VAR>hI : I ≠ ⊥<VAR>K : Ideal T<GOAL>Multiset.count K (UniqueFactorizationMonoid.normalizedFactors J) ≤ Multiset.count K (UniqueFactorizationMonoid.normalizedFactors I)
<VAR>T : Type u_4<VAR>CommRing T<VAR>IsDedekindDomain T<VAR>I J : Ideal T<VAR>hI : I ≠ ⊥<VAR>hJ : J ≠ ⊥<GOAL>I ⊔ J = (UniqueFactorizationMonoid.normalizedFactors I ∩ UniqueFactorizationMonoid.normalizedFactors J).prod
<VAR>T : Type u_4<VAR>CommRing T<VAR>IsDedekindDomain T<VAR>I J : Ideal T<VAR>hI : I ≠ ⊥<VAR>hJ : Irreducible J<VAR>n : ℕ<GOAL>J ^ n ⊔ I = J ^ min (Multiset.count J (UniqueFactorizationMonoid.normalizedFactors I)) n
<VAR>T : Type u_4<VAR>CommRing T<VAR>IsDedekindDomain T<VAR>I J : Ideal T<VAR>hJ : Irreducible J<VAR>n : ℕ<VAR>hn : ↑n ≤ multiplicity J I<GOAL>J ^ n ⊔ I = J ^ n
<VAR>T : Type u_4<VAR>CommRing T<VAR>IsDedekindDomain T<VAR>I J : Ideal T<VAR>hI : I ≠ ⊥<VAR>hJ : Irreducible J<VAR>n : ℕ<VAR>hn : multiplicity J I ≤ ↑n<GOAL>J ^ n ⊔ I = J ^ (multiplicity J I).get ⋯
<VAR>R : Type u_1<VAR>CommRing R<VAR>self : IsDedekindDomain.HeightOneSpectrum R<GOAL>self.asIdeal ≠ ⊥
<VAR>R : Type u_1<VAR>CommRing R<VAR>self : IsDedekindDomain.HeightOneSpectrum R<GOAL>self.asIdeal.IsPrime
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<GOAL>Prime v.asIdeal
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<GOAL>Irreducible v.asIdeal
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<GOAL>Irreducible (Associates.mk v.asIdeal)
<VAR>R : Type u_1<VAR>K : Type u_3<VAR>CommRing R<VAR>Field K<VAR>IsDedekindDomain R<VAR>Algebra R K<VAR>hK : IsFractionRing R K<GOAL>⨅ v, Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯ = ⊥
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>IsDedekindDomain A<VAR>I : Ideal R<VAR>J : Ideal A<VAR>f : R ⧸ I →+* A ⧸ J<VAR>hf : Function.Surjective ⇑f<VAR>X : { p // p ∣ I }<GOAL>↑((idealFactorsFunOfQuotHom hf) X) = Ideal.comap (Ideal.Quotient.mk J) (Ideal.map f (Ideal.map (Ideal.Quotient.mk I) ↑X))
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDedekindDomain A<VAR>J : Ideal A<GOAL>idealFactorsFunOfQuotHom ⋯ = OrderHom.id
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>IsDedekindDomain A<VAR>I : Ideal R<VAR>J : Ideal A<VAR>B : Type u_4<VAR>CommRing B<VAR>IsDedekindDomain B<VAR>L : Ideal B<VAR>f : R ⧸ I →+* A ⧸ J<VAR>g : A ⧸ J →+* B ⧸ L<VAR>hf : Function.Surjective ⇑f<VAR>hg : Function.Surjective ⇑g<GOAL>(idealFactorsFunOfQuotHom hg).comp (idealFactorsFunOfQuotHom hf) = idealFactorsFunOfQuotHom ⋯
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>IsDedekindDomain A<VAR>I : Ideal R<VAR>J : Ideal A<VAR>IsDedekindDomain R<VAR>f : R ⧸ I ≃+* A ⧸ J<GOAL>(idealFactorsEquivOfQuotEquiv f).symm = idealFactorsEquivOfQuotEquiv f.symm
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>IsDedekindDomain A<VAR>I : Ideal R<VAR>J : Ideal A<VAR>IsDedekindDomain R<VAR>f : R ⧸ I ≃+* A ⧸ J<VAR>L M : Ideal R<VAR>hL : L ∣ I<VAR>hM : M ∣ I<GOAL>↑((idealFactorsEquivOfQuotEquiv f) ⟨L, hL⟩) ∣ ↑((idealFactorsEquivOfQuotEquiv f) ⟨M, hM⟩) ↔ L ∣ M
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>IsDedekindDomain A<VAR>I : Ideal R<VAR>J : Ideal A<VAR>IsDedekindDomain R<VAR>f : R ⧸ I ≃+* A ⧸ J<VAR>hJ : J ≠ ⊥<VAR>L : Ideal R<VAR>hL : L ∈ UniqueFactorizationMonoid.normalizedFactors I<GOAL>↑((idealFactorsEquivOfQuotEquiv f) ⟨L, ⋯⟩) ∈ UniqueFactorizationMonoid.normalizedFactors J
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>IsDedekindDomain A<VAR>I : Ideal R<VAR>J : Ideal A<VAR>IsDedekindDomain R<VAR>f : R ⧸ I ≃+* A ⧸ J<VAR>hI : I ≠ ⊥<VAR>hJ : J ≠ ⊥<GOAL>(normalizedFactorsEquivOfQuotEquiv f hI hJ).symm = normalizedFactorsEquivOfQuotEquiv f.symm hJ hI
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>IsDedekindDomain A<VAR>I : Ideal R<VAR>J : Ideal A<VAR>IsDedekindDomain R<VAR>f : R ⧸ I ≃+* A ⧸ J<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>hI : I ≠ ⊥<VAR>hJ : J ≠ ⊥<VAR>L : Ideal R<VAR>hL : L ∈ UniqueFactorizationMonoid.normalizedFactors I<GOAL>multiplicity (↑((normalizedFactorsEquivOfQuotEquiv f hI hJ) ⟨L, hL⟩)) J = multiplicity L I
<VAR>R : Type u_1<VAR>CommRing R<VAR>Ring.DimensionLEOne R<VAR>P Q : Ideal R<VAR>hP : P.IsPrime<VAR>hQ : Q.IsPrime<VAR>hP0 : P ≠ ⊥<GOAL>P ≤ Q ↔ P = Q
<VAR>R : Type u_1<VAR>CommRing R<VAR>I J : Ideal R<VAR>h : ∀ (P : Ideal R), I ≤ P → J ≤ P → ¬P.IsPrime<GOAL>IsCoprime I J
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>a b : R<VAR>n : ℕ<VAR>h : a * b ∈ I ^ n<GOAL>a ∈ I ∨ b ∈ I ^ n
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>a b : R<VAR>n : ℕ<VAR>h : a * b ∈ I ^ n<GOAL>a ∈ I ^ n ∨ b ∈ I