ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>r : ι → F<VAR>x : F<VAR>hvs : Set.InjOn v ↑s<VAR>hs : s.Nonempty<VAR>hx : ∀ i ∈ s, x ≠ v i<GOAL>Polynomial.eval x ((Lagrange.interpolate s v) r) = (∑ i ∈ s, Lagrange.nodalWeight s v i * (x - v i)⁻¹ * r i) / ∑ i ∈ s, Lagrange.nodalWeight s v i * (x - v i)⁻¹
<VAR>R : Type uR<VAR>A : Type uA<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>CommRing R<VAR>CommRing A<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Algebra R A<VAR>Module R M₁<VAR>Module A M₁<VAR>SMulCommClass R A M₁<VAR>IsScalarTower R A M₁<VAR>Module R M₂<VAR>Invertible 2<VAR>Q₁ : QuadraticForm A M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>m₁ : M₁<VAR>m₂ : M₂<GOAL>((QuadraticForm.tensorDistrib R A) (Q₁ ⊗ₜ[R] Q₂)) (m₁ ⊗ₜ[R] m₂) = Q₂ m₂ • Q₁ m₁
<VAR>R : Type uR<VAR>A : Type uA<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>CommRing R<VAR>CommRing A<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Algebra R A<VAR>Module R M₁<VAR>Module A M₁<VAR>SMulCommClass R A M₁<VAR>IsScalarTower R A M₁<VAR>Module R M₂<VAR>Invertible 2<VAR>Invertible 2<VAR>Q₁ : QuadraticForm A M₁<VAR>Q₂ : QuadraticForm R M₂<GOAL>QuadraticMap.associated (Q₁.tmul Q₂) = (QuadraticMap.associated Q₁).tmul (QuadraticMap.associated Q₂)
<VAR>R : Type uR<VAR>A : Type uA<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>CommRing R<VAR>CommRing A<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Algebra R A<VAR>Module R M₁<VAR>Module A M₁<VAR>SMulCommClass R A M₁<VAR>IsScalarTower R A M₁<VAR>Module R M₂<VAR>Invertible 2<VAR>Invertible 2<VAR>Q₁ : QuadraticForm A M₁<VAR>Q₂ : QuadraticForm R M₂<GOAL>QuadraticMap.polarBilin (Q₁.tmul Q₂) = ⅟2 • (QuadraticMap.polarBilin Q₁).tmul (QuadraticMap.polarBilin Q₂)
<VAR>R : Type uR<VAR>A : Type uA<VAR>M₂ : Type uM₂<VAR>CommRing R<VAR>CommRing A<VAR>AddCommGroup M₂<VAR>Algebra R A<VAR>Module R M₂<VAR>Invertible 2<VAR>Q : QuadraticForm R M₂<VAR>a : A<VAR>m₂ : M₂<GOAL>(QuadraticForm.baseChange A Q) (a ⊗ₜ[R] m₂) = Q m₂ • (a * a)
<VAR>R : Type uR<VAR>A : Type uA<VAR>M₂ : Type uM₂<VAR>CommRing R<VAR>CommRing A<VAR>AddCommGroup M₂<VAR>Algebra R A<VAR>Module R M₂<VAR>Invertible 2<VAR>Invertible 2<VAR>Q : QuadraticForm R M₂<GOAL>QuadraticMap.associated (QuadraticForm.baseChange A Q) = LinearMap.BilinMap.baseChange A (QuadraticMap.associated Q)
<VAR>R : Type uR<VAR>A : Type uA<VAR>M₂ : Type uM₂<VAR>CommRing R<VAR>CommRing A<VAR>AddCommGroup M₂<VAR>Algebra R A<VAR>Module R M₂<VAR>Invertible 2<VAR>Invertible 2<VAR>Q : QuadraticForm R M₂<GOAL>QuadraticMap.polarBilin (QuadraticForm.baseChange A Q) = LinearMap.BilinMap.baseChange A (QuadraticMap.polarBilin Q)
<VAR>R : Type uR<VAR>A : Type uA<VAR>M₂ : Type uM₂<VAR>CommRing R<VAR>CommRing A<VAR>AddCommGroup M₂<VAR>Algebra R A<VAR>Module R M₂<VAR>Q₁ Q₂ : QuadraticForm A (A ⊗[R] M₂)<VAR>h : ∀ (m : M₂), Q₁ (1 ⊗ₜ[R] m) = Q₂ (1 ⊗ₜ[R] m)<GOAL>Q₁ = Q₂
<VAR>k : Type u_1<VAR>Ring k<VAR>V : Type u_2<VAR>P : Type u_3<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>v : V<VAR>s : AffineSubspace k P<GOAL>v +ᵥ s = AffineSubspace.map (↑(AffineEquiv.constVAdd k P v)) s
<VAR>k : Type u_1<VAR>Ring k<VAR>V : Type u_2<VAR>P : Type u_3<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>v : V<VAR>s : AffineSubspace k P<GOAL>↑(v +ᵥ s) = v +ᵥ ↑s
<VAR>k : Type u_1<VAR>Ring k<VAR>V : Type u_2<VAR>P : Type u_3<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>v : V<VAR>s : AffineSubspace k P<VAR>p : P<GOAL>v +ᵥ p ∈ v +ᵥ s ↔ p ∈ s
<VAR>k : Type u_1<VAR>Ring k<VAR>V : Type u_2<VAR>P : Type u_3<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>v : V<GOAL>v +ᵥ ⊥ = ⊥
<VAR>k : Type u_1<VAR>Ring k<VAR>V : Type u_2<VAR>P : Type u_3<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>v : V<GOAL>v +ᵥ ⊤ = ⊤
<VAR>k : Type u_1<VAR>Ring k<VAR>V : Type u_2<VAR>P : Type u_3<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>v : V<VAR>s : AffineSubspace k P<GOAL>(v +ᵥ s).direction = s.direction
<VAR>k : Type u_1<VAR>Ring k<VAR>V : Type u_2<VAR>P : Type u_3<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>v : V<VAR>s : Set P<GOAL>v +ᵥ affineSpan k s = affineSpan k (v +ᵥ s)
<VAR>k : Type u_1<VAR>Ring k<VAR>V₁ : Type u_4<VAR>P₁ : Type u_5<VAR>V₂ : Type u_6<VAR>P₂ : Type u_7<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>f : P₁ →ᵃ[k] P₂<VAR>v : V₁<VAR>s : AffineSubspace k P₁<GOAL>AffineSubspace.map f (v +ᵥ s) = f.linear v +ᵥ AffineSubspace.map f s
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b : AffineBasis ι k P<VAR>ι' : Type u_1<VAR>q : ι' → P<VAR>i : ι'<VAR>j : ι<GOAL>b.toMatrix q i j = (b.coord j) (q i)
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b : AffineBasis ι k P<VAR>DecidableEq ι<GOAL>b.toMatrix ⇑b = 1
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b : AffineBasis ι k P<VAR>ι' : Type u_1<VAR>Fintype ι<VAR>q : ι' → P<VAR>i : ι'<GOAL>∑ j : ι, b.toMatrix q i j = 1
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b : AffineBasis ι k P<VAR>ι' : Type u_1<VAR>Fintype ι<VAR>Finite ι'<VAR>DecidableEq ι'<VAR>p : ι' → P<VAR>A : Matrix ι ι' k<VAR>hA : b.toMatrix p * A = 1<GOAL>AffineIndependent k p
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b : AffineBasis ι k P<VAR>ι' : Type u_1<VAR>Finite ι<VAR>Fintype ι'<VAR>DecidableEq ι<VAR>Nontrivial k<VAR>p : ι' → P<VAR>A : Matrix ι ι' k<VAR>hA : A * b.toMatrix p = 1<GOAL>affineSpan k (Set.range p) = ⊤
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b : AffineBasis ι k P<VAR>Fintype ι<VAR>b₂ : AffineBasis ι k P<VAR>x : P<GOAL>b₂.coords x ᵥ* b.toMatrix ⇑b₂ = b.coords x
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b : AffineBasis ι k P<VAR>Fintype ι<VAR>b₂ : AffineBasis ι k P<VAR>DecidableEq ι<GOAL>b.toMatrix ⇑b₂ * b₂.toMatrix ⇑b = 1
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b : AffineBasis ι k P<VAR>Fintype ι<VAR>b₂ : AffineBasis ι k P<VAR>DecidableEq ι<GOAL>IsUnit (b.toMatrix ⇑b₂)
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>Ring k<VAR>Module k V<VAR>b : AffineBasis ι k P<VAR>Fintype ι<VAR>DecidableEq ι<VAR>Nontrivial k<VAR>p : ι → P<GOAL>IsUnit (b.toMatrix p) ↔ AffineIndependent k p ∧ affineSpan k (Set.range p) = ⊤
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>CommRing k<VAR>Module k V<VAR>DecidableEq ι<VAR>Fintype ι<VAR>b b₂ : AffineBasis ι k P<VAR>x : P<GOAL>b.coords x ᵥ* (b.toMatrix ⇑b₂)⁻¹ = b₂.coords x
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>CommRing k<VAR>Module k V<VAR>DecidableEq ι<VAR>Fintype ι<VAR>b b₂ : AffineBasis ι k P<VAR>x : P<GOAL>(b.toMatrix ⇑b₂).det • b₂.coords x = (b.toMatrix ⇑b₂)ᵀ.cramer (b.coords x)
<VAR>R : Type u<VAR>M : Type v₁<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : Module.Dual R M<VAR>m : M<GOAL>(contractLeft R M) (f ⊗ₜ[R] m) = f m
<VAR>R : Type u<VAR>M : Type v₁<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : Module.Dual R M<VAR>m : M<GOAL>(contractRight R M) (m ⊗ₜ[R] f) = f m
<VAR>R : Type u<VAR>M : Type v₁<VAR>N : Type v₂<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>f : Module.Dual R M<VAR>m : M<VAR>n : N<GOAL>((dualTensorHom R M N) (f ⊗ₜ[R] n)) m = f m • n
<VAR>R : Type u<VAR>M : Type v₁<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : Module.Dual R M<VAR>m : M<GOAL>Module.Dual.transpose ((dualTensorHom R M M) (f ⊗ₜ[R] m)) = (dualTensorHom R (Module.Dual R M) (Module.Dual R M)) ((Module.Dual.eval R M) m ⊗ₜ[R] f)
<VAR>R : Type u<VAR>M : Type v₁<VAR>N : Type v₂<VAR>P : Type v₃<VAR>Q : Type v₄<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>f : Module.Dual R M<VAR>p : P<GOAL>((dualTensorHom R M P) (f ⊗ₜ[R] p)).prodMap 0 = (dualTensorHom R (M × N) (P × Q)) ((f ∘ₗ LinearMap.fst R M N) ⊗ₜ[R] (LinearMap.inl R P Q) p)
<VAR>R : Type u<VAR>M : Type v₁<VAR>N : Type v₂<VAR>P : Type v₃<VAR>Q : Type v₄<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>g : Module.Dual R N<VAR>q : Q<GOAL>LinearMap.prodMap 0 ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) = (dualTensorHom R (M × N) (P × Q)) ((g ∘ₗ LinearMap.snd R M N) ⊗ₜ[R] (LinearMap.inr R P Q) q)
<VAR>R : Type u<VAR>M : Type v₁<VAR>N : Type v₂<VAR>P : Type v₃<VAR>Q : Type v₄<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>f : Module.Dual R M<VAR>p : P<VAR>g : Module.Dual R N<VAR>q : Q<GOAL>TensorProduct.map ((dualTensorHom R M P) (f ⊗ₜ[R] p)) ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) = (dualTensorHom R (TensorProduct R M N) (TensorProduct R P Q)) ((TensorProduct.dualDistrib R M N) (f ⊗ₜ[R] g) ⊗ₜ[R] p ⊗ₜ[R] q)
<VAR>R : Type u<VAR>M : Type v₁<VAR>N : Type v₂<VAR>P : Type v₃<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : Module.Dual R M<VAR>n : N<VAR>g : Module.Dual R N<VAR>p : P<GOAL>(dualTensorHom R N P) (g ⊗ₜ[R] p) ∘ₗ (dualTensorHom R M N) (f ⊗ₜ[R] n) = g n • (dualTensorHom R M P) (f ⊗ₜ[R] p)
<VAR>R : Type u<VAR>M : Type v₁<VAR>N : Type v₂<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>m : Type u_1<VAR>n : Type u_2<VAR>Fintype m<VAR>Finite n<VAR>DecidableEq m<VAR>DecidableEq n<VAR>bM : Basis m R M<VAR>bN : Basis n R N<VAR>j : m<VAR>i : n<GOAL>(LinearMap.toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) = Matrix.stdBasisMatrix i j 1
<VAR>ι : Type w<VAR>R : Type u<VAR>M : Type v₁<VAR>N : Type v₂<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>DecidableEq ι<VAR>Fintype ι<VAR>b : Basis ι R M<VAR>x : TensorProduct R (Module.Dual R M) N<GOAL>(dualTensorHomEquivOfBasis b) x = (dualTensorHom R M N) x
<VAR>ι : Type w<VAR>R : Type u<VAR>M : Type v₁<VAR>N : Type v₂<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>DecidableEq ι<VAR>Fintype ι<VAR>b : Basis ι R M<GOAL>↑(dualTensorHomEquivOfBasis b) = dualTensorHom R M N
<VAR>ι : Type w<VAR>R : Type u<VAR>M : Type v₁<VAR>N : Type v₂<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>DecidableEq ι<VAR>Fintype ι<VAR>b : Basis ι R M<VAR>x : TensorProduct R (Module.Dual R M) N<GOAL>(dualTensorHomEquivOfBasis b).symm ((dualTensorHom R M N) x) = x
<VAR>ι : Type w<VAR>R : Type u<VAR>M : Type v₁<VAR>N : Type v₂<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>DecidableEq ι<VAR>Fintype ι<VAR>b : Basis ι R M<VAR>x : M →ₗ[R] N<GOAL>(dualTensorHom R M N) ((dualTensorHomEquivOfBasis b).symm x) = x
<VAR>R : Type u<VAR>M : Type v₁<VAR>P : Type v₃<VAR>Q : Type v₄<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup P<VAR>AddCommGroup Q<VAR>Module R M<VAR>Module R P<VAR>Module R Q<VAR>Module.Free R M<VAR>Module.Finite R M<GOAL>↑(lTensorHomEquivHomLTensor R M P Q) = TensorProduct.lTensorHomToHomLTensor R M P Q
<VAR>R : Type u<VAR>M : Type v₁<VAR>P : Type v₃<VAR>Q : Type v₄<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup P<VAR>AddCommGroup Q<VAR>Module R M<VAR>Module R P<VAR>Module R Q<VAR>Module.Free R M<VAR>Module.Finite R M<GOAL>↑(rTensorHomEquivHomRTensor R M P Q) = TensorProduct.rTensorHomToHomRTensor R M P Q
<VAR>R : Type u<VAR>M : Type v₁<VAR>P : Type v₃<VAR>Q : Type v₄<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup P<VAR>AddCommGroup Q<VAR>Module R M<VAR>Module R P<VAR>Module R Q<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>x : TensorProduct R P (M →ₗ[R] Q)<GOAL>(lTensorHomEquivHomLTensor R M P Q) x = (TensorProduct.lTensorHomToHomLTensor R M P Q) x
<VAR>R : Type u<VAR>M : Type v₁<VAR>P : Type v₃<VAR>Q : Type v₄<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup P<VAR>AddCommGroup Q<VAR>Module R M<VAR>Module R P<VAR>Module R Q<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>x : TensorProduct R (M →ₗ[R] P) Q<GOAL>(rTensorHomEquivHomRTensor R M P Q) x = (TensorProduct.rTensorHomToHomRTensor R M P Q) x
<VAR>R : Type u<VAR>M : Type v₁<VAR>N : Type v₂<VAR>P : Type v₃<VAR>Q : Type v₄<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>AddCommGroup Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>Module.Free R N<VAR>Module.Finite R N<GOAL>↑(homTensorHomEquiv R M N P Q) = TensorProduct.homTensorHomMap R M N P Q
<VAR>R : Type u<VAR>M : Type v₁<VAR>N : Type v₂<VAR>P : Type v₃<VAR>Q : Type v₄<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>AddCommGroup Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>Module.Free R N<VAR>Module.Finite R N<VAR>x : TensorProduct R (M →ₗ[R] P) (N →ₗ[R] Q)<GOAL>(homTensorHomEquiv R M N P Q) x = (TensorProduct.homTensorHomMap R M N P Q) x
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>AddCommGroup V₂<VAR>Module k V₁<VAR>Module k V₂<VAR>AddTorsor V₁ P₁<VAR>AddTorsor V₂ P₂<VAR>E : AffineSubspace k P₁<VAR>Ene : Nonempty ↥E<VAR>φ : P₁ →ᵃ[k] P₂<GOAL>Nonempty ↥(AffineSubspace.map φ E)
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>AddCommGroup V₂<VAR>Module k V₁<VAR>Module k V₂<VAR>AddTorsor V₁ P₁<VAR>AddTorsor V₂ P₂<VAR>φ : P₁ →ᵃ[k] P₂<VAR>E : AffineSubspace k P₁<VAR>F : AffineSubspace k P₂<VAR>Nonempty ↥E<VAR>Nonempty ↥F<VAR>hEF : AffineSubspace.map φ E ≤ F<VAR>x : ↥E<GOAL>↑((φ.restrict hEF) x) = φ ↑x
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>AddCommGroup V₂<VAR>Module k V₁<VAR>Module k V₂<VAR>AddTorsor V₁ P₁<VAR>AddTorsor V₂ P₂<VAR>φ : P₁ →ᵃ[k] P₂<VAR>E : AffineSubspace k P₁<VAR>F : AffineSubspace k P₂<VAR>hEF : AffineSubspace.map φ E ≤ F<GOAL>E.direction ≤ Submodule.comap φ.linear F.direction
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>AddCommGroup V₂<VAR>Module k V₁<VAR>Module k V₂<VAR>AddTorsor V₁ P₁<VAR>AddTorsor V₂ P₂<VAR>φ : P₁ →ᵃ[k] P₂<VAR>E : AffineSubspace k P₁<VAR>F : AffineSubspace k P₂<VAR>Nonempty ↥E<VAR>Nonempty ↥F<VAR>hEF : AffineSubspace.map φ E ≤ F<GOAL>(φ.restrict hEF).linear = φ.linear.restrict ⋯
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>AddCommGroup V₂<VAR>Module k V₁<VAR>Module k V₂<VAR>AddTorsor V₁ P₁<VAR>AddTorsor V₂ P₂<VAR>φ : P₁ →ᵃ[k] P₂<VAR>hφ : Function.Injective ⇑φ<VAR>E : AffineSubspace k P₁<VAR>F : AffineSubspace k P₂<VAR>Nonempty ↥E<VAR>Nonempty ↥F<VAR>hEF : AffineSubspace.map φ E ≤ F<GOAL>Function.Injective ⇑(φ.restrict hEF)
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>AddCommGroup V₂<VAR>Module k V₁<VAR>Module k V₂<VAR>AddTorsor V₁ P₁<VAR>AddTorsor V₂ P₂<VAR>φ : P₁ →ᵃ[k] P₂<VAR>E : AffineSubspace k P₁<VAR>F : AffineSubspace k P₂<VAR>Nonempty ↥E<VAR>Nonempty ↥F<VAR>h : AffineSubspace.map φ E = F<GOAL>Function.Surjective ⇑(φ.restrict ⋯)
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>AddCommGroup V₂<VAR>Module k V₁<VAR>Module k V₂<VAR>AddTorsor V₁ P₁<VAR>AddTorsor V₂ P₂<VAR>E : AffineSubspace k P₁<VAR>Nonempty ↥E<VAR>φ : P₁ →ᵃ[k] P₂<VAR>hφ : Function.Injective ⇑φ<GOAL>Function.Bijective ⇑(φ.restrict ⋯)
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M N : Submodule R S<GOAL>M.LinearDisjoint N ↔ Function.Injective ⇑(M.mulMap N)
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>self : M.LinearDisjoint N<GOAL>Function.Injective ⇑(M.mulMap N)
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>m : ↥M<VAR>n : ↥N<GOAL>↑(H.mulMap (m ⊗ₜ[R] n)) = ↑m * ↑n
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>Subsingleton R<GOAL>M.LinearDisjoint N
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M N : Submodule R S<GOAL>M.LinearDisjoint N ↔ (Submodule.equivOpposite.symm (MulOpposite.op N)).LinearDisjoint (Submodule.equivOpposite.symm (MulOpposite.op M))
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>hc : ∀ (m : ↥M) (n : ↥N), Commute ↑m ↑n<GOAL>N.LinearDisjoint M
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>hc : ∀ (m : ↥M) (n : ↥N), Commute ↑m ↑n<GOAL>M.LinearDisjoint N ↔ N.LinearDisjoint M
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>ι : Type u_1<VAR>m : Basis ι R ↥M<VAR>H : Function.Injective ⇑(Submodule.mulLeftMap N ⇑m)<GOAL>M.LinearDisjoint N
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>ι : Type u_1<VAR>n : Basis ι R ↥N<VAR>H : Function.Injective ⇑(M.mulRightMap ⇑n)<GOAL>M.LinearDisjoint N
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>κ : Type u_1<VAR>ι : Type u_2<VAR>m : Basis κ R ↥M<VAR>n : Basis ι R ↥N<VAR>H : Function.Injective ⇑(Finsupp.total (κ × ι) S R fun i => ↑(m i.1) * ↑(n i.2))<GOAL>M.LinearDisjoint N
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>N : Submodule R S<GOAL>⊥.LinearDisjoint N
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M : Submodule R S<GOAL>M.LinearDisjoint ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>N : Submodule R S<GOAL>Submodule.LinearDisjoint 1 N
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M : Submodule R S<GOAL>M.LinearDisjoint 1
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>H : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N<GOAL>M.LinearDisjoint N
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'<GOAL>M.LinearDisjoint N
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>H : ∀ (M' N' : Submodule R S), M' ≤ M → N' ≤ N → M'.FG → N'.FG → M'.LinearDisjoint N'<GOAL>M.LinearDisjoint N
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<GOAL>N.LinearDisjoint M
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>M N : Submodule R S<GOAL>M.LinearDisjoint N ↔ N.LinearDisjoint M
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>Module.Flat R ↥N<VAR>ι : Type u_1<VAR>m : ι → ↥M<VAR>hm : LinearIndependent R m<GOAL>LinearMap.ker (Submodule.mulLeftMap N m) = ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>ι : Type u_1<VAR>m : Basis ι R ↥M<VAR>H : LinearMap.ker (Submodule.mulLeftMap N ⇑m) = ⊥<GOAL>M.LinearDisjoint N
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>Module.Flat R ↥M<VAR>ι : Type u_1<VAR>n : ι → ↥N<VAR>hn : LinearIndependent R n<GOAL>LinearMap.ker (M.mulRightMap n) = ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>ι : Type u_1<VAR>n : Basis ι R ↥N<VAR>H : LinearMap.ker (M.mulRightMap ⇑n) = ⊥<GOAL>M.LinearDisjoint N
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>Module.Flat R ↥M<VAR>κ : Type u_1<VAR>ι : Type u_2<VAR>m : κ → ↥M<VAR>n : ι → ↥N<VAR>hm : LinearIndependent R m<VAR>hn : LinearIndependent R n<GOAL>LinearIndependent R fun i => ↑(m i.1) * ↑(n i.2)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>Module.Flat R ↥N<VAR>κ : Type u_1<VAR>ι : Type u_2<VAR>m : κ → ↥M<VAR>n : ι → ↥N<VAR>hm : LinearIndependent R m<VAR>hn : LinearIndependent R n<GOAL>LinearIndependent R fun i => ↑(m i.1) * ↑(n i.2)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>hf : Module.Flat R ↥M ∨ Module.Flat R ↥N<VAR>κ : Type u_1<VAR>ι : Type u_2<VAR>m : κ → ↥M<VAR>n : ι → ↥N<VAR>hm : LinearIndependent R m<VAR>hn : LinearIndependent R n<GOAL>LinearIndependent R fun i => ↑(m i.1) * ↑(n i.2)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>κ : Type u_1<VAR>ι : Type u_2<VAR>m : Basis κ R ↥M<VAR>n : Basis ι R ↥N<VAR>H : LinearIndependent R fun i => ↑(m i.1) * ↑(n i.2)<GOAL>M.LinearDisjoint N
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>M' : Submodule R S<VAR>h : M' ≤ M<VAR>Module.Flat R ↥N<GOAL>M'.LinearDisjoint N
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>N' : Submodule R S<VAR>h : N' ≤ N<VAR>Module.Flat R ↥M<GOAL>M.LinearDisjoint N'
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>M' N' : Submodule R S<VAR>hm : M' ≤ M<VAR>hn : N' ≤ N<VAR>Module.Flat R ↥N<VAR>Module.Flat R ↥M'<GOAL>M'.LinearDisjoint N'
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>M' N' : Submodule R S<VAR>hm : M' ≤ M<VAR>hn : N' ≤ N<VAR>Module.Flat R ↥M<VAR>Module.Flat R ↥N'<GOAL>M'.LinearDisjoint N'
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>h : M ≤ 1<VAR>Module.Flat R ↥N<GOAL>M.LinearDisjoint N
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>h : N ≤ 1<VAR>Module.Flat R ↥M<GOAL>M.LinearDisjoint N
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>Nontrivial R<VAR>Module.Flat R ↥M<VAR>a b : ↥(M ⊓ N)<VAR>hc : Commute ↑a ↑b<GOAL>¬LinearIndependent R ![a, b]
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>Nontrivial R<VAR>Module.Flat R ↥N<VAR>a b : ↥(M ⊓ N)<VAR>hc : Commute ↑a ↑b<GOAL>¬LinearIndependent R ![a, b]
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>Nontrivial R<VAR>hf : Module.Flat R ↥M ∨ Module.Flat R ↥N<VAR>a b : ↥(M ⊓ N)<VAR>hc : Commute ↑a ↑b<GOAL>¬LinearIndependent R ![a, b]
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>hf : Module.Flat R ↥M ∨ Module.Flat R ↥N<VAR>hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n<GOAL>Module.rank R ↥(M ⊓ N) ≤ 1