ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type uR<VAR>M : Type uM<VAR>ι : Type uι<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>DecidableEq ι<VAR>b : Basis ι R M<VAR>m₁ m₂ : M<GOAL>(b.toDualFlip m₁) m₂ = (b.toDual m₂) m₁
<VAR>R : Type uR<VAR>M : Type uM<VAR>ι : Type uι<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>DecidableEq ι<VAR>b : Basis ι R M<VAR>Finite ι<VAR>m : M<VAR>i : ι<GOAL>(b.toDual m) (b i) = b.equivFun m i
<VAR>R : Type uR<VAR>M : Type uM<VAR>ι : Type uι<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>DecidableEq ι<VAR>b : Basis ι R M<GOAL>Function.Injective ⇑b.toDual
<VAR>R : Type uR<VAR>M : Type uM<VAR>ι : Type uι<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>DecidableEq ι<VAR>b : Basis ι R M<VAR>m : M<VAR>a : b.toDual m = 0<GOAL>m = 0
<VAR>R : Type uR<VAR>M : Type uM<VAR>ι : Type uι<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>DecidableEq ι<VAR>b : Basis ι R M<GOAL>LinearMap.ker b.toDual = ⊥
<VAR>R : Type uR<VAR>M : Type uM<VAR>ι : Type uι<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>DecidableEq ι<VAR>b : Basis ι R M<VAR>Finite ι<GOAL>LinearMap.range b.toDual = ⊤
<VAR>R : Type uR<VAR>M : Type uM<VAR>ι : Type uι<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Fintype ι<VAR>b : Basis ι R M<VAR>f : Module.Dual R M<GOAL>∑ x : ι, f (b x) • b.coord x = f
<VAR>R : Type uR<VAR>M : Type uM<VAR>ι : Type uι<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>DecidableEq ι<VAR>b : Basis ι R M<VAR>Finite ι<VAR>m : M<GOAL>b.toDualEquiv m = b.toDual m
<VAR>K : Type uK<VAR>V : Type uV<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<GOAL>Nonempty (V ≃ₗ[K] Module.Dual K V) ↔ FiniteDimensional K V
<VAR>R : Type uR<VAR>M : Type uM<VAR>ι : Type uι<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>DecidableEq ι<VAR>b : Basis ι R M<VAR>Finite ι<VAR>i j : ι<GOAL>(b.dualBasis i) (b j) = if j = i then 1 else 0
<VAR>R : Type uR<VAR>M : Type uM<VAR>ι : Type uι<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>DecidableEq ι<VAR>b : Basis ι R M<VAR>Finite ι<VAR>f : ι →₀ R<VAR>i : ι<GOAL>((Finsupp.total ι (Module.Dual R M) R ⇑b.dualBasis) f) (b i) = f i
<VAR>R : Type uR<VAR>M : Type uM<VAR>ι : Type uι<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>DecidableEq ι<VAR>b : Basis ι R M<VAR>Finite ι<VAR>l : Module.Dual R M<VAR>i : ι<GOAL>(b.dualBasis.repr l) i = l (b i)
<VAR>R : Type uR<VAR>M : Type uM<VAR>ι : Type uι<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>DecidableEq ι<VAR>b : Basis ι R M<VAR>Finite ι<VAR>i : ι<VAR>m : M<GOAL>(b.dualBasis i) m = (b.repr m) i
<VAR>R : Type uR<VAR>M : Type uM<VAR>ι : Type uι<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>DecidableEq ι<VAR>b : Basis ι R M<VAR>Finite ι<GOAL>⇑b.dualBasis = b.coord
<VAR>R : Type uR<VAR>M : Type uM<VAR>ι : Type uι<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>DecidableEq ι<VAR>b : Basis ι R M<VAR>Finite ι<GOAL>b.dualBasis.toDual ∘ₗ b.toDual = Module.Dual.eval R M
<VAR>R : Type uR<VAR>M : Type uM<VAR>ι : Type uι<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>DecidableEq ι<VAR>b : Basis ι R M<VAR>Finite ι<VAR>l : Module.Dual R M<VAR>i : ι<GOAL>b.dualBasis.equivFun l i = l (b i)
<VAR>R : Type uR<VAR>M : Type uM<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_1<VAR>b : Basis ι R M<GOAL>LinearMap.ker (Module.Dual.eval R M) = ⊥
<VAR>R : Type uR<VAR>M : Type uM<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_1<VAR>Finite ι<VAR>b : Basis ι R M<GOAL>LinearMap.range (Module.Dual.eval R M) = ⊤
<VAR>R : Type uR<VAR>M : Type uM<VAR>ι : Type uι<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Finite ι<VAR>b : Basis ι R M<VAR>f : ι →₀ R<VAR>i : ι<GOAL>((Finsupp.total ι (Module.Dual R M) R b.coord) f) (b i) = f i
<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>CommRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>Finite ι<VAR>b : Basis ι K V<GOAL>Cardinal.lift.{uK, uV} (Module.rank K V) = Module.rank K (Module.Dual K V)
<VAR>K : Type uK<VAR>V : Type uV<VAR>CommRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>Module.Free K V<GOAL>LinearMap.ker (Module.Dual.eval K V) = ⊥
<VAR>K : Type uK<VAR>V : Type uV<VAR>CommRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>Module.Free K V<GOAL>Function.Injective (Submodule.map (Module.Dual.eval K V))
<VAR>K : Type uK<VAR>V : Type uV<VAR>CommRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>Module.Free K V<GOAL>Function.Surjective (Submodule.comap (Module.Dual.eval K V))
<VAR>K : Type uK<VAR>V : Type uV<VAR>CommRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>Module.Free K V<VAR>v : V<GOAL>(Module.Dual.eval K V) v = 0 ↔ v = 0
<VAR>K : Type uK<VAR>V : Type uV<VAR>CommRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>Module.Free K V<GOAL>Function.Injective ⇑(Module.Dual.eval K V)
<VAR>K : Type uK<VAR>V : Type uV<VAR>CommRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>Module.Free K V<VAR>v : V<GOAL>(∀ (φ : Module.Dual K V), φ v = 0) ↔ v = 0
<VAR>K : Type uK<VAR>V : Type uV<VAR>CommRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>Module.Free K V<GOAL>Subsingleton (Module.Dual K V) ↔ Subsingleton V
<VAR>K : Type uK<VAR>V : Type uV<VAR>CommRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>Module.Free K V<GOAL>Nontrivial (Module.Dual K V) ↔ Nontrivial V
<VAR>K : Type uK<VAR>V : Type uV<VAR>CommRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>Module.Free K V<GOAL>Module.Finite K (Module.Dual K V) ↔ Module.Finite K V
<VAR>K : Type uK<VAR>V : Type uV<VAR>CommRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>Module.Free K V<VAR>Module.Finite K V<GOAL>Cardinal.lift.{uK, uV} (Module.rank K V) = Module.rank K (Module.Dual K V)
<VAR>K : Type uK<VAR>V : Type uV<VAR>CommRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>Module.Free K V<VAR>Module.Finite K V<GOAL>LinearMap.range (Module.Dual.eval K V) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>self : Module.IsReflexive R M<GOAL>Function.Bijective ⇑(Module.Dual.eval R M)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.IsReflexive R M<GOAL>Function.Bijective ⇑(Module.Dual.eval R M)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.IsReflexive R M<GOAL>↑(Module.evalEquiv R M) = Module.Dual.eval R M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.IsReflexive R M<VAR>m : M<GOAL>(Module.evalEquiv R M) m = (Module.Dual.eval R M) m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.IsReflexive R M<VAR>f : Module.Dual R M<VAR>g : Module.Dual R (Module.Dual R M)<GOAL>f ((Module.evalEquiv R M).symm g) = g f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.IsReflexive R M<GOAL>↑(Module.evalEquiv R M).symm.dualMap = Module.Dual.eval R (Module.Dual R M)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.IsReflexive R M<VAR>W : Submodule R M<GOAL>(Module.mapEvalEquiv R M) W = Submodule.map (Module.Dual.eval R M) W
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.IsReflexive R M<VAR>W'' : Submodule R (Module.Dual R (Module.Dual R M))<GOAL>(Module.mapEvalEquiv R M).symm W'' = Submodule.comap (Module.Dual.eval R M) W''
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Module.IsReflexive R M<VAR>e : M ≃ₗ[R] N<GOAL>Module.IsReflexive R N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>x : M<VAR>hx : x ∉ p<VAR>hp' : Module.Free R (M ⧸ p)<GOAL>∃ f, f x ≠ 0 ∧ Submodule.map f p = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>hp : p < ⊤<VAR>hp' : Module.Free R (M ⧸ p)<GOAL>∃ f, f ≠ 0 ∧ Submodule.map f p = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>DecidableEq ι<VAR>e : ι → M<VAR>ε : ι → Module.Dual R M<VAR>self : Module.DualBases e ε<VAR>m : M<GOAL>(∀ (i : ι), (ε i) m = 0) → m = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>DecidableEq ι<VAR>e : ι → M<VAR>ε : ι → Module.Dual R M<VAR>self : Module.DualBases e ε<VAR>i j : ι<GOAL>(ε i) (e j) = if i = j then 1 else 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>DecidableEq ι<VAR>e : ι → M<VAR>ε : ι → Module.Dual R M<VAR>self : Module.DualBases e ε<VAR>m : M<GOAL>{i | (ε i) m ≠ 0}.Finite
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>e : ι → M<VAR>ε : ι → Module.Dual R M<VAR>DecidableEq ι<VAR>h : Module.DualBases e ε<VAR>m : M<VAR>i : ι<GOAL>(h.coeffs m) i = (ε i) m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>e : ι → M<VAR>l : ι →₀ R<GOAL>Module.DualBases.lc e l = (Finsupp.total ι M R e) l
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>e : ι → M<VAR>ε : ι → Module.Dual R M<VAR>DecidableEq ι<VAR>h : Module.DualBases e ε<VAR>l : ι →₀ R<VAR>i : ι<GOAL>(ε i) (Module.DualBases.lc e l) = l i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>e : ι → M<VAR>ε : ι → Module.Dual R M<VAR>DecidableEq ι<VAR>h : Module.DualBases e ε<VAR>l : ι →₀ R<GOAL>h.coeffs (Module.DualBases.lc e l) = l
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>e : ι → M<VAR>ε : ι → Module.Dual R M<VAR>DecidableEq ι<VAR>h : Module.DualBases e ε<VAR>m : M<GOAL>Module.DualBases.lc e (h.coeffs m) = m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>e : ι → M<VAR>ε : ι → Module.Dual R M<VAR>DecidableEq ι<VAR>h : Module.DualBases e ε<VAR>m : M<GOAL>h.basis.repr m = h.coeffs m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>e : ι → M<VAR>ε : ι → Module.Dual R M<VAR>DecidableEq ι<VAR>h : Module.DualBases e ε<VAR>l : ι →₀ R<GOAL>h.basis.repr.symm l = Module.DualBases.lc e l
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>e : ι → M<VAR>ε : ι → Module.Dual R M<VAR>DecidableEq ι<VAR>h : Module.DualBases e ε<GOAL>⇑h.basis = e
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>e : ι → M<VAR>ε : ι → Module.Dual R M<VAR>DecidableEq ι<VAR>h : Module.DualBases e ε<VAR>H : Set ι<VAR>x : M<VAR>hmem : x ∈ Submodule.span R (e '' H)<VAR>i : ι<GOAL>(ε i) x ≠ 0 → i ∈ H
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>e : ι → M<VAR>ε : ι → Module.Dual R M<VAR>DecidableEq ι<VAR>h : Module.DualBases e ε<VAR>Finite ι<GOAL>⇑h.basis.dualBasis = ε
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>W : Submodule R M<GOAL>W.dualRestrict = W.subtype.dualMap
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>W : Submodule R M<VAR>φ : Module.Dual R M<VAR>x : ↥W<GOAL>(W.dualRestrict φ) x = φ ↑x
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>W : Submodule R M<VAR>φ : Module.Dual R M<GOAL>φ ∈ W.dualAnnihilator ↔ ∀ w ∈ W, φ w = 0
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>W : Submodule R M<GOAL>LinearMap.ker W.dualRestrict = W.dualAnnihilator
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Φ : Submodule R (Module.Dual R M)<VAR>x : M<GOAL>x ∈ Φ.dualCoannihilator ↔ ∀ φ ∈ Φ, φ x = 0
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Φ : Submodule R (Module.Dual R M)<GOAL>Submodule.comap (Module.Dual.eval R M) Φ.dualAnnihilator = Φ.dualCoannihilator
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Φ : Submodule R (Module.Dual R M)<GOAL>Submodule.map (Module.Dual.eval R M) Φ.dualCoannihilator ≤ Φ.dualAnnihilator
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>GaloisConnection (⇑OrderDual.toDual ∘ Submodule.dualAnnihilator) (Submodule.dualCoannihilator ∘ ⇑OrderDual.ofDual)
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>U : Submodule R (Module.Dual R M)<VAR>V : Submodule R M<GOAL>U ≤ V.dualAnnihilator ↔ V ≤ U.dualCoannihilator
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>⊥.dualAnnihilator = ⊤
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>⊤.dualAnnihilator = ⊥
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>⊥.dualCoannihilator = ⊤
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>U V : Submodule R M<VAR>hUV : U ≤ V<GOAL>V.dualAnnihilator ≤ U.dualAnnihilator
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>U V : Submodule R (Module.Dual R M)<VAR>hUV : U ≤ V<GOAL>V.dualCoannihilator ≤ U.dualCoannihilator
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>U : Submodule R M<GOAL>U ≤ U.dualAnnihilator.dualCoannihilator
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>U : Submodule R (Module.Dual R M)<GOAL>U ≤ U.dualCoannihilator.dualAnnihilator
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>U : Submodule R M<GOAL>U.dualAnnihilator.dualCoannihilator.dualAnnihilator = U.dualAnnihilator
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>U : Submodule R (Module.Dual R M)<GOAL>U.dualCoannihilator.dualAnnihilator.dualCoannihilator = U.dualCoannihilator
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>U V : Submodule R M<GOAL>(U ⊔ V).dualAnnihilator = U.dualAnnihilator ⊓ V.dualAnnihilator
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>U V : Submodule R (Module.Dual R M)<GOAL>(U ⊔ V).dualCoannihilator = U.dualCoannihilator ⊓ V.dualCoannihilator
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Sort u_1<VAR>U : ι → Submodule R M<GOAL>(⨆ i, U i).dualAnnihilator = ⨅ i, (U i).dualAnnihilator
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Sort u_1<VAR>U : ι → Submodule R (Module.Dual R M)<GOAL>(⨆ i, U i).dualCoannihilator = ⨅ i, (U i).dualCoannihilator
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>U V : Submodule R M<GOAL>U.dualAnnihilator ⊔ V.dualAnnihilator ≤ (U ⊓ V).dualAnnihilator
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Sort u_1<VAR>U : ι → Submodule R M<GOAL>⨆ i, (U i).dualAnnihilator ≤ (⨅ i, U i).dualAnnihilator
<VAR>K : Type u<VAR>V : Type v<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>W : Subspace K V<GOAL>Submodule.dualCoannihilator ⊤ = ⊥
<VAR>K : Type u<VAR>V : Type v<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>W : Subspace K V<GOAL>(Submodule.dualAnnihilator W).dualCoannihilator = W
<VAR>K : Type u<VAR>V : Type v<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>W : Subspace K V<VAR>v : V<GOAL>(∀ φ ∈ Submodule.dualAnnihilator W, φ v = 0) ↔ v ∈ W
<VAR>K : Type u<VAR>V : Type v<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>W : Subspace K V<GOAL>Submodule.comap (Module.Dual.eval K V) (Submodule.dualAnnihilator W).dualAnnihilator = W
<VAR>K : Type u<VAR>V : Type v<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>W : Subspace K V<GOAL>Submodule.map (Module.Dual.eval K V) W ≤ (Submodule.dualAnnihilator W).dualAnnihilator
<VAR>K : Type u<VAR>V : Type v<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>W W' : Subspace K V<GOAL>Submodule.dualAnnihilator W ≤ Submodule.dualAnnihilator W' ↔ W' ≤ W
<VAR>K : Type u<VAR>V : Type v<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>W W' : Subspace K V<GOAL>Submodule.dualAnnihilator W = Submodule.dualAnnihilator W' ↔ W = W'
<VAR>K : Type u<VAR>V : Type v<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>W : Subspace K V<VAR>φ : Module.Dual K ↥W<VAR>w : ↥W<GOAL>(W.dualLift φ) ↑w = φ w
<VAR>K : Type u<VAR>V : Type v<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>W : Subspace K V<VAR>φ : Module.Dual K ↥W<VAR>w : V<VAR>hw : w ∈ W<GOAL>(W.dualLift φ) w = φ ⟨w, hw⟩
<VAR>K : Type u<VAR>V : Type v<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>W : Subspace K V<GOAL>Submodule.dualRestrict W ∘ₗ W.dualLift = 1
<VAR>K : Type u<VAR>V : Type v<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>W : Subspace K V<GOAL>Function.LeftInverse ⇑(Submodule.dualRestrict W) ⇑W.dualLift
<VAR>K : Type u<VAR>V : Type v<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>W : Subspace K V<GOAL>Function.RightInverse ⇑W.dualLift ⇑(Submodule.dualRestrict W)
<VAR>K : Type u<VAR>V : Type v<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>W : Subspace K V<GOAL>Function.Surjective ⇑(Submodule.dualRestrict W)
<VAR>K : Type u<VAR>V : Type v<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>W : Subspace K V<GOAL>Function.Injective ⇑W.dualLift
<VAR>K : Type u<VAR>V : Type v<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>W : Subspace K V<VAR>φ : Module.Dual K V<GOAL>W.quotAnnihilatorEquiv (Submodule.Quotient.mk φ) = (Submodule.dualRestrict W) φ
<VAR>K : Type u<VAR>V : Type v<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>W : Subspace K V<GOAL>↑W.dualEquivDual = W.dualLift.rangeRestrict
<VAR>K : Type u<VAR>V : Type v<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>W : Subspace K V<VAR>φ : Module.Dual K ↥W<GOAL>W.dualEquivDual φ = ⟨W.dualLift φ, ⋯⟩
<VAR>K : Type u<VAR>V : Type v<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<GOAL>FiniteDimensional.finrank K (Module.Dual K V) = FiniteDimensional.finrank K V
<VAR>K : Type u<VAR>V : Type v<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>W : Subspace K V<GOAL>(Submodule.dualAnnihilator W).dualAnnihilator = (Module.mapEvalEquiv K V) W
<VAR>K : Type u<VAR>V : Type v<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>Φ : Subspace K (Module.Dual K V)<GOAL>FiniteDimensional.finrank K ↥(Submodule.dualCoannihilator Φ) = FiniteDimensional.finrank K ↥(Submodule.dualAnnihilator Φ)
<VAR>K : Type u<VAR>V : Type v<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>W : Subspace K (Module.Dual K V)<GOAL>FiniteDimensional.finrank K ↥W + FiniteDimensional.finrank K ↥(Submodule.dualCoannihilator W) = FiniteDimensional.finrank K V
<VAR>R : Type uR<VAR>CommSemiring R<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>f : M₁ →ₗ[R] M₂<GOAL>LinearMap.ker f.dualMap = (LinearMap.range f).dualAnnihilator
<VAR>R : Type uR<VAR>CommSemiring R<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>f : M₁ →ₗ[R] M₂<GOAL>LinearMap.range f.dualMap ≤ (LinearMap.ker f).dualAnnihilator
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>W : Submodule R M<VAR>φ : ↥W.dualAnnihilator<VAR>x : M<GOAL>(W.dualCopairing φ) (Submodule.Quotient.mk x) = φ x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>W : Submodule R M<VAR>φ : Module.Dual R M<VAR>x : ↥W<GOAL>(W.dualPairing (Submodule.Quotient.mk φ)) x = φ ↑x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>W : Submodule R M<GOAL>LinearMap.range W.mkQ.dualMap = W.dualAnnihilator
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>W : Submodule R M<VAR>φ : Module.Dual R (M ⧸ W)<VAR>x : M<GOAL>(W.dualQuotEquivDualAnnihilator φ) x = φ (Submodule.Quotient.mk x)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>W : Submodule R M<GOAL>W.dualCopairing = ↑W.dualQuotEquivDualAnnihilator.symm
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>W : Submodule R M<VAR>φ : ↥W.dualAnnihilator<VAR>x : M<GOAL>(W.dualQuotEquivDualAnnihilator.symm φ) (Submodule.Quotient.mk x) = φ x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>W : Submodule R M<VAR>Module.Free R (M ⧸ W)<GOAL>Module.Finite R ↥W.dualAnnihilator ↔ Module.Finite R (M ⧸ W)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>W : Submodule R (Module.Dual R M)<VAR>m : M<VAR>w : ↥W<GOAL>(W.quotDualCoannihilatorToDual (Submodule.Quotient.mk m)) w = ↑w m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>W : Submodule R (Module.Dual R M)<GOAL>Function.Injective ⇑W.quotDualCoannihilatorToDual
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>W : Submodule R (Module.Dual R M)<GOAL>Function.Injective ⇑W.quotDualCoannihilatorToDual.flip
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>W : Submodule R (Module.Dual R M)<GOAL>W.quotDualCoannihilatorToDual.Nondegenerate
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>hf : Function.Surjective ⇑f<GOAL>LinearMap.range f.dualMap = (LinearMap.ker f).dualAnnihilator
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>hf : Function.Surjective ⇑(LinearMap.range f).subtype.dualMap<GOAL>LinearMap.range f.dualMap = (LinearMap.ker f).dualAnnihilator
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>f : M →ₗ[R] M'<GOAL>LinearMap.ker f.dualMap = (LinearMap.range (Module.Dual.eval R M' ∘ₗ f)).dualCoannihilator
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>B : M →ₗ[R] M' →ₗ[R] R<GOAL>(LinearMap.range B).dualCoannihilator = LinearMap.ker B.flip
<VAR>K : Type uK<VAR>Field K<VAR>V₁ : Type uV₁<VAR>AddCommGroup V₁<VAR>Module K V₁<VAR>f : Module.Dual K V₁<VAR>hf : f ≠ 0<GOAL>LinearMap.range f = ⊤
<VAR>K : Type uK<VAR>Field K<VAR>V₁ : Type uV₁<VAR>AddCommGroup V₁<VAR>Module K V₁<VAR>FiniteDimensional K V₁<VAR>f : Module.Dual K V₁<VAR>hf : f ≠ 0<GOAL>FiniteDimensional.finrank K ↥(LinearMap.ker f) + 1 = FiniteDimensional.finrank K V₁
<VAR>K : Type uK<VAR>Field K<VAR>V₁ : Type uV₁<VAR>AddCommGroup V₁<VAR>Module K V₁<VAR>FiniteDimensional K V₁<VAR>f : Module.Dual K V₁<VAR>hf : f ≠ 0<VAR>p : Submodule K V₁<VAR>hpf : Disjoint (LinearMap.ker f) p<VAR>hp : p ≠ ⊥<GOAL>IsCompl (LinearMap.ker f) p
<VAR>K : Type uK<VAR>Field K<VAR>V₁ : Type uV₁<VAR>AddCommGroup V₁<VAR>Module K V₁<VAR>FiniteDimensional K V₁<VAR>f g : Module.Dual K V₁<VAR>x : V₁<VAR>h : LinearMap.ker f = LinearMap.ker g<VAR>h' : f x = g x<VAR>hx : f x ≠ 0<GOAL>f = g
<VAR>K : Type uK<VAR>Field K<VAR>V₁ : Type uV₁<VAR>AddCommGroup V₁<VAR>Module K V₁<GOAL>(Module.dualPairing K V₁).Nondegenerate
<VAR>K : Type uK<VAR>Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>AddCommGroup V₁<VAR>Module K V₁<VAR>AddCommGroup V₂<VAR>Module K V₂<VAR>f : V₁ →ₗ[K] V₂<VAR>hf : Function.Injective ⇑f<GOAL>Function.Surjective ⇑f.dualMap
<VAR>K : Type uK<VAR>Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>AddCommGroup V₁<VAR>Module K V₁<VAR>AddCommGroup V₂<VAR>Module K V₂<VAR>f : V₁ →ₗ[K] V₂<GOAL>LinearMap.range f.dualMap = (LinearMap.ker f).dualAnnihilator
<VAR>K : Type uK<VAR>Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>AddCommGroup V₁<VAR>Module K V₁<VAR>AddCommGroup V₂<VAR>Module K V₂<VAR>f : V₁ →ₗ[K] V₂<GOAL>Function.Surjective ⇑f.dualMap ↔ Function.Injective ⇑f
<VAR>K : Type uK<VAR>Field K<VAR>V₁ : Type uV₁<VAR>AddCommGroup V₁<VAR>Module K V₁<VAR>W : Subspace K V₁<GOAL>Submodule.dualPairing W = ↑W.quotAnnihilatorEquiv