ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>i : ι<VAR>f : N<GOAL>(P.coreflection i) f = f - (P.toLin (P.root i)) f • P.coroot i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>i j : ι<GOAL>(P.coreflection i) (P.coroot j) = P.coroot j - P.pairing i j • P.coroot i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>i : ι<GOAL>(P.coreflection i) (P.coroot i) = -P.coroot i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>i : ι<VAR>x : N<GOAL>(P.coreflection i) ((P.coreflection i) x) = x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>i : ι<GOAL>Set.BijOn (⇑(P.coreflection i)) (Set.range ⇑P.coroot) (Set.range ⇑P.coroot)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>i : ι<GOAL>⇑(P.coreflection i) '' Set.range ⇑P.coroot = Set.range ⇑P.coroot
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>i : ι<GOAL>P.coreflection i = P.flip.reflection i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>i : ι<GOAL>↑(P.reflection i).dualMap ∘ₗ P.toLin.flip = P.toLin.flip ∘ₗ ↑(P.coreflection i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>i j k : ι<VAR>hk : P.root k = (P.reflection i) (P.root j)<GOAL>P.coroot k = (P.coreflection i) (P.coroot j)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<GOAL>P.IsCrystallographic ↔ ∀ (i j : ι), ∃ z, ↑z = P.pairing i j
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<GOAL>P.IsReduced ↔ ∀ (i j : ι), i ≠ j → ¬LinearIndependent R ![P.root i, P.root j] → P.root i = -P.root j
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>i j : ι<GOAL>P.coxeterWeight i j = P.coxeterWeight j i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>i j : ι<GOAL>P.IsOrthogonal i j ↔ P.IsOrthogonal j i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>i j : ι<VAR>h : P.IsOrthogonal i j<GOAL>Commute (P.reflection i) (P.reflection j)
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>U : Submodule R M<VAR>x y : M<GOAL>x ≡ y [SMOD U] ↔ Submodule.Quotient.mk x = Submodule.Quotient.mk y
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>U : Submodule R M<VAR>x y : M<GOAL>x ≡ y [SMOD U] ↔ x - y ∈ U
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>x y : M<GOAL>x ≡ y [SMOD ⊤]
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>x y : M<GOAL>x ≡ y [SMOD ⊥] ↔ x = y
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>U₁ U₂ : Submodule R M<VAR>x y : M<VAR>HU : U₁ ≤ U₂<VAR>hxy : x ≡ y [SMOD U₁]<GOAL>x ≡ y [SMOD U₂]
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>U : Submodule R M<VAR>x : M<GOAL>x ≡ x [SMOD U]
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>U : Submodule R M<VAR>x y : M<VAR>hxy : x ≡ y [SMOD U]<GOAL>y ≡ x [SMOD U]
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>U : Submodule R M<VAR>x y z : M<VAR>hxy : x ≡ y [SMOD U]<VAR>hyz : y ≡ z [SMOD U]<GOAL>x ≡ z [SMOD U]
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>U : Submodule R M<VAR>x₁ x₂ y₁ y₂ : M<VAR>hxy₁ : x₁ ≡ y₁ [SMOD U]<VAR>hxy₂ : x₂ ≡ y₂ [SMOD U]<GOAL>x₁ + x₂ ≡ y₁ + y₂ [SMOD U]
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>U : Submodule R M<VAR>x y : M<VAR>hxy : x ≡ y [SMOD U]<VAR>c : R<GOAL>c • x ≡ c • y [SMOD U]
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>U : Submodule R M<VAR>x y : M<VAR>hxy : x ≡ y [SMOD U]<VAR>n : ℕ<GOAL>n • x ≡ n • y [SMOD U]
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>U : Submodule R M<VAR>x y : M<VAR>hxy : x ≡ y [SMOD U]<VAR>n : ℤ<GOAL>n • x ≡ n • y [SMOD U]
<VAR>A : Type u_2<VAR>CommRing A<VAR>I : Ideal A<VAR>x₁ x₂ y₁ y₂ : A<VAR>hxy₁ : x₁ ≡ y₁ [SMOD I]<VAR>hxy₂ : x₂ ≡ y₂ [SMOD I]<GOAL>x₁ * x₂ ≡ y₁ * y₂ [SMOD I]
<VAR>A : Type u_2<VAR>CommRing A<VAR>I : Ideal A<VAR>x y : A<VAR>n : ℕ<VAR>hxy : x ≡ y [SMOD I]<GOAL>x ^ n ≡ y ^ n [SMOD I]
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>U : Submodule R M<VAR>x y : M<VAR>hxy : x ≡ y [SMOD U]<GOAL>-x ≡ -y [SMOD U]
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>U : Submodule R M<VAR>x₁ x₂ y₁ y₂ : M<VAR>hxy₁ : x₁ ≡ y₁ [SMOD U]<VAR>hxy₂ : x₂ ≡ y₂ [SMOD U]<GOAL>x₁ - x₂ ≡ y₁ - y₂ [SMOD U]
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>U : Submodule R M<VAR>x : M<GOAL>x ≡ 0 [SMOD U] ↔ x ∈ U
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>U : Submodule R M<VAR>x y : M<VAR>N : Type u_4<VAR>AddCommGroup N<VAR>Module R N<VAR>hxy : x ≡ y [SMOD U]<VAR>f : M →ₗ[R] N<GOAL>f x ≡ f y [SMOD Submodule.map f U]
<VAR>R : Type u_1<VAR>Ring R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>x y : M<VAR>N : Type u_4<VAR>AddCommGroup N<VAR>Module R N<VAR>V : Submodule R N<VAR>f : M →ₗ[R] N<VAR>hxy : f x ≡ f y [SMOD V]<GOAL>x ≡ y [SMOD Submodule.comap f V]
<VAR>R : Type u_5<VAR>CommRing R<VAR>I : Ideal R<VAR>x y : R<VAR>h : x ≡ y [SMOD I]<VAR>f : R[X]<GOAL>Polynomial.eval x f ≡ Polynomial.eval y f [SMOD I]
<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>I : Submodule B L<VAR>x : L<GOAL>x ∈ Submodule.traceDual A K I ↔ ∀ a ∈ I, ((Algebra.traceForm K L) x) a ∈ (algebraMap A K).range
<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>I J : Submodule B L<GOAL>I ≤ Submodule.traceDual A K J ↔ Submodule.map (↑A (Algebra.trace K L)) (Submodule.restrictScalars A (I * J)) ≤ 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>I J J' : Submodule B L<GOAL>I ≤ Submodule.traceDual A K (J * J') ↔ I * J ≤ Submodule.traceDual A K J'
<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>I J : Submodule B L<GOAL>I ≤ Submodule.traceDual A K J ↔ I * J ≤ Submodule.traceDual 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>I J : Submodule B L<GOAL>I ≤ Submodule.traceDual A K J ↔ J ≤ Submodule.traceDual A K I
<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>I : Submodule B L<GOAL>I ≤ Submodule.traceDual A K (Submodule.traceDual A K I)
<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<GOAL>Submodule.traceDual A K ⊥ = ⊤
<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<GOAL>Submodule.traceDual A K ⊤ = if Submodule.restrictScalars A (LinearMap.range (Algebra.trace K L)) ≤ 1 then ⊤ else ⊥
<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>FiniteDimensional K L<VAR>Algebra.IsSeparable K L<VAR>Decidable (IsField A)<GOAL>Submodule.traceDual A K ⊤ = if IsField A then ⊤ else ⊥
<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>IsFractionRing A K<VAR>IsIntegrallyClosed A<VAR>I : Submodule B L<VAR>x : L<GOAL>x ∈ Submodule.traceDual A K I ↔ ∀ a ∈ I, IsIntegral A (((Algebra.traceForm K L) x) a)
<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>IsFractionRing A K<VAR>IsIntegralClosure B A L<VAR>FiniteDimensional K L<VAR>IsIntegrallyClosed A<GOAL>1 ≤ Submodule.traceDual 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>IsFractionRing A K<VAR>IsIntegralClosure B A L<VAR>FiniteDimensional K L<VAR>Algebra.IsSeparable K L<VAR>IsIntegrallyClosed A<VAR>I : Submodule B L<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>Fintype ι<VAR>b : Basis ι K L<VAR>hb : ∀ (i : ι), IsIntegral A (b i)<VAR>a x : L<VAR>ha : a ∈ I<VAR>hx : x ∈ Submodule.traceDual A K I<GOAL>IsIntegral A (Algebra.discr K ⇑b • 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>IsFractionRing B L<VAR>IsDomain B<VAR>NoZeroSMulDivisors A B<VAR>I : Submodule B (FractionRing B)<GOAL>Submodule.map (FractionRing.algEquiv B L) (Submodule.traceDual A (FractionRing A) I) = Submodule.traceDual A K (Submodule.map (FractionRing.algEquiv B L) I)
<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<GOAL>↑(FractionalIdeal.dual A K I) = Submodule.traceDual A K ↑I
<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<GOAL>↑(FractionalIdeal.dual A K 1) = Submodule.traceDual 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<GOAL>FractionalIdeal.dual A K 0 = 0
<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>x : L<GOAL>x ∈ FractionalIdeal.dual A K I ↔ ∀ a ∈ I, ((Algebra.traceForm K L) x) a ∈ (algebraMap A K).range
<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<GOAL>FractionalIdeal.dual A K I ≠ 0
<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<GOAL>FractionalIdeal.dual A K I = 0 ↔ I = 0
<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<GOAL>FractionalIdeal.dual A K I ≠ 0 ↔ I ≠ 0
<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 J : FractionalIdeal B⁰ L<VAR>hI : I ≠ 0<VAR>hIJ : I * J ≤ 1<GOAL>J ≤ FractionalIdeal.dual A K I
<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<GOAL>1 ≤ 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 J : FractionalIdeal B⁰ L<VAR>hJ : J ≠ 0<GOAL>I ≤ FractionalIdeal.dual A K J ↔ I * J ≤ 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<GOAL>I⁻¹ ≤ FractionalIdeal.dual A K I
<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<GOAL>(FractionalIdeal.dual A K I)⁻¹ ≤ I
<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<GOAL>FractionalIdeal.dual A K I = FractionalIdeal.dual A K 1 * I⁻¹
<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 J : FractionalIdeal B⁰ L<GOAL>FractionalIdeal.dual A K J / FractionalIdeal.dual A K I = I / J
<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<GOAL>FractionalIdeal.dual A K I * I = 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<GOAL>I * FractionalIdeal.dual A K I = 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<GOAL>FractionalIdeal.dual A K I⁻¹ = FractionalIdeal.dual A K 1 * I
<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<GOAL>FractionalIdeal.dual A K (FractionalIdeal.dual A K I) = I
<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 J : FractionalIdeal B⁰ L<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<GOAL>FractionalIdeal.dual A K I ≤ FractionalIdeal.dual A K J ↔ J ≤ I
<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<GOAL>Function.Involutive (FractionalIdeal.dual A K)
<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<GOAL>Function.Injective (FractionalIdeal.dual A K)
<VAR>A : Type u_1<VAR>B : Type u_3<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>IsDomain A<VAR>IsIntegrallyClosed A<VAR>IsDedekindDomain B<VAR>NoZeroSMulDivisors A B<VAR>Algebra.IsIntegral A B<VAR>Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>FiniteDimensional (FractionRing A) (FractionRing B)<GOAL>IsLocalization.coeSubmodule (FractionRing B) (differentIdeal A B) = 1 / Submodule.traceDual A (FractionRing A) 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>NoZeroSMulDivisors A B<GOAL>IsLocalization.coeSubmodule L (differentIdeal A B) = 1 / Submodule.traceDual A K 1