ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>Q : QuadraticMap R M N<VAR>x y : M<GOAL>Q.IsOrtho x y ↔ Q (x + y) = Q x + Q y
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>x y : M<GOAL>QuadraticMap.IsOrtho 0 x y
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>Q : QuadraticMap R M N<VAR>x : M<GOAL>Q.IsOrtho 0 x
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>Q : QuadraticMap R M N<VAR>x : M<GOAL>Q.IsOrtho x 0
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>Q : QuadraticMap R M N<VAR>x : M<VAR>hx₁ : ¬Q.IsOrtho x x<GOAL>x ≠ 0
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>Q : QuadraticMap R M N<VAR>x y : M<GOAL>Q.IsOrtho x y ↔ Q.IsOrtho y x
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>IsCancelAdd R<VAR>NoZeroDivisors R<VAR>CharZero R<VAR>B : LinearMap.BilinMap R M R<VAR>x y : M<VAR>h : LinearMap.IsSymm B<GOAL>B.toQuadraticMap.IsOrtho x y ↔ LinearMap.IsOrtho B x y
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>Q : QuadraticMap R M N<VAR>x y : M<GOAL>LinearMap.IsOrtho Q.polarBilin x y ↔ Q.IsOrtho x y
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>Q : QuadraticMap R M N<VAR>x y : M<VAR>h : Q.IsOrtho x y<GOAL>QuadraticMap.polar (⇑Q) x y = 0
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>Q : QuadraticMap R M N<VAR>Invertible 2<VAR>x y : M<GOAL>LinearMap.IsOrtho (QuadraticMap.associated Q) x y ↔ Q.IsOrtho x y
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticMap R M N<GOAL>¬Q.Anisotropic ↔ ∃ x, x ≠ 0 ∧ Q x = 0
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticMap R M N<VAR>h : Q.Anisotropic<VAR>x : M<GOAL>Q x = 0 ↔ x = 0
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Invertible 2<VAR>Q : QuadraticMap R M R<VAR>hB : Q.Anisotropic<GOAL>LinearMap.SeparatingLeft (QuadraticMap.associated' Q)
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>PartialOrder N<VAR>AddCommMonoid N<VAR>R : Type u_8<VAR>LinearOrderedCommRing R<VAR>Module R M<VAR>Module R N<VAR>PosSMulStrictMono R N<VAR>Q : QuadraticMap R M N<VAR>h : Q.PosDef<VAR>a : R<VAR>a_pos : 0 < a<GOAL>(a • Q).PosDef
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>R₂ : Type u<VAR>CommSemiring R₂<VAR>AddCommMonoid M<VAR>Module R₂ M<VAR>PartialOrder N<VAR>AddCommMonoid N<VAR>Module R₂ N<VAR>Q : QuadraticMap R₂ M N<VAR>hQ : Q.PosDef<VAR>x : M<GOAL>0 ≤ Q x
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>R₂ : Type u<VAR>CommSemiring R₂<VAR>AddCommMonoid M<VAR>Module R₂ M<VAR>PartialOrder N<VAR>AddCommMonoid N<VAR>Module R₂ N<VAR>Q : QuadraticMap R₂ M N<VAR>hQ : Q.PosDef<GOAL>Q.Anisotropic
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>R₂ : Type u<VAR>CommSemiring R₂<VAR>AddCommMonoid M<VAR>Module R₂ M<VAR>PartialOrder N<VAR>AddCommMonoid N<VAR>Module R₂ N<VAR>Q : QuadraticMap R₂ M N<VAR>h : ∀ (x : M), 0 ≤ Q x<VAR>h0 : Q.Anisotropic<GOAL>Q.PosDef
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>R₂ : Type u<VAR>CommSemiring R₂<VAR>AddCommMonoid M<VAR>Module R₂ M<VAR>PartialOrder N<VAR>AddCommMonoid N<VAR>Module R₂ N<VAR>Q : QuadraticMap R₂ M N<GOAL>Q.PosDef ↔ (∀ (x : M), 0 ≤ Q x) ∧ Q.Anisotropic
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>R₂ : Type u<VAR>CommSemiring R₂<VAR>AddCommMonoid M<VAR>Module R₂ M<VAR>PartialOrder N<VAR>AddCommMonoid N<VAR>Module R₂ N<VAR>CovariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>Q Q' : QuadraticMap R₂ M N<VAR>hQ : Q.PosDef<VAR>hQ' : Q'.PosDef<GOAL>(Q + Q').PosDef
<VAR>M : Type u_4<VAR>A : Type u_7<VAR>AddCommMonoid M<VAR>R : Type u_9<VAR>LinearOrderedCommRing R<VAR>Module R M<VAR>LinearOrderedSemiring A<VAR>ExistsAddOfLE A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>f : M →ₗ[R] A<VAR>hf : LinearMap.ker f = ⊥<GOAL>(QuadraticMap.linMulLin f f).PosDef
<VAR>R : Type u_3<VAR>n : Type w<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing R<VAR>Invertible 2<VAR>a : R<VAR>Q : QuadraticMap R (n → R) R<GOAL>(a • Q).toMatrix' = a • Q.toMatrix'
<VAR>R : Type u_3<VAR>n : Type w<VAR>Fintype n<VAR>DecidableEq n<VAR>CommRing R<VAR>Invertible 2<VAR>Q : QuadraticMap R (n → R) R<GOAL>Q.toMatrix'.IsSymm
<VAR>R : Type u_3<VAR>n : Type w<VAR>Fintype n<VAR>CommRing R<VAR>DecidableEq n<VAR>Invertible 2<VAR>m : Type w<VAR>DecidableEq m<VAR>Fintype m<VAR>Q : QuadraticMap R (m → R) R<VAR>f : (n → R) →ₗ[R] m → R<GOAL>(Q.comp f).toMatrix' = (LinearMap.toMatrix' f).transpose * Q.toMatrix' * LinearMap.toMatrix' f
<VAR>R : Type u_3<VAR>n : Type w<VAR>Fintype n<VAR>CommRing R<VAR>DecidableEq n<VAR>Invertible 2<VAR>Q : QuadraticMap R (n → R) R<VAR>a : R<GOAL>(a • Q).discr = a ^ Fintype.card n * Q.discr
<VAR>R : Type u_3<VAR>n : Type w<VAR>Fintype n<VAR>CommRing R<VAR>DecidableEq n<VAR>Invertible 2<VAR>Q : QuadraticMap R (n → R) R<VAR>f : (n → R) →ₗ[R] n → R<GOAL>(Q.comp f).discr = (LinearMap.toMatrix' f).det * (LinearMap.toMatrix' f).det * Q.discr
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>hB : (LinearMap.BilinMap.toQuadraticMap B).Anisotropic<GOAL>LinearMap.SeparatingLeft B
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>htwo : Invertible 2<VAR>B : LinearMap.BilinForm R M<VAR>hB₁ : B ≠ 0<VAR>hB₂ : LinearMap.IsSymm B<GOAL>∃ x, ¬LinearMap.IsOrtho B x x
<VAR>V : Type u<VAR>K : Type v<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>hK : Invertible 2<VAR>B : LinearMap.BilinForm K V<VAR>hB₂ : LinearMap.IsSymm B<GOAL>∃ v, LinearMap.IsOrthoᵢ B ⇑v
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>ι : Type u_8<VAR>Fintype ι<VAR>v : Basis ι R M<VAR>Q : QuadraticMap R M N<VAR>w : ι → R<GOAL>(Q.basisRepr v) w = Q (∑ i : ι, w i • v i)
<VAR>S : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>ι : Type u_8<VAR>Fintype ι<VAR>Monoid S<VAR>DistribMulAction S R<VAR>SMulCommClass S R R<VAR>w : ι → S<VAR>v : ι → R<GOAL>(QuadraticMap.weightedSumSquares R w) v = ∑ i : ι, w i • (v i * v i)
<VAR>ι : Type u_8<VAR>Fintype ι<VAR>R : Type u_9<VAR>M : Type u_10<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Invertible 2<VAR>Q : QuadraticMap R M R<VAR>v : Basis ι R M<VAR>hv₂ : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑v<GOAL>Q.basisRepr v = QuadraticMap.weightedSumSquares R fun i => Q (v i)
<VAR>R : Type u<VAR>M₂ : Type w<VAR>ι : Type x<VAR>Semiring R<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>φ : ι → Type i<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>f : (i : ι) → M₂ →ₗ[R] φ i<VAR>c : M₂<VAR>i : ι<GOAL>(LinearMap.pi f) c i = (f i) c
<VAR>R : Type u<VAR>M₂ : Type w<VAR>ι : Type x<VAR>Semiring R<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>φ : ι → Type i<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>f : (i : ι) → M₂ →ₗ[R] φ i<GOAL>LinearMap.ker (LinearMap.pi f) = ⨅ i, LinearMap.ker (f i)
<VAR>R : Type u<VAR>M₂ : Type w<VAR>ι : Type x<VAR>Semiring R<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>φ : ι → Type i<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>f : (i : ι) → M₂ →ₗ[R] φ i<GOAL>LinearMap.pi f = 0 ↔ ∀ (i : ι), f i = 0
<VAR>R : Type u<VAR>M₂ : Type w<VAR>ι : Type x<VAR>Semiring R<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>φ : ι → Type i<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<GOAL>(LinearMap.pi fun i => 0) = 0
<VAR>R : Type u<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>ι : Type x<VAR>Semiring R<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>AddCommMonoid M₃<VAR>Module R M₃<VAR>φ : ι → Type i<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>f : (i : ι) → M₂ →ₗ[R] φ i<VAR>g : M₃ →ₗ[R] M₂<GOAL>LinearMap.pi f ∘ₗ g = LinearMap.pi fun i => f i ∘ₗ g
<VAR>R : Type u<VAR>ι : Type x<VAR>Semiring R<VAR>φ : ι → Type i<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>i : ι<GOAL>⇑(LinearMap.proj i) = Function.eval i
<VAR>R : Type u<VAR>ι : Type x<VAR>Semiring R<VAR>φ : ι → Type i<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>i : ι<VAR>b : (i : ι) → φ i<GOAL>(LinearMap.proj i) b = b i
<VAR>R : Type u<VAR>M₂ : Type w<VAR>ι : Type x<VAR>Semiring R<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>φ : ι → Type i<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>f : (i : ι) → M₂ →ₗ[R] φ i<VAR>i : ι<GOAL>LinearMap.proj i ∘ₗ LinearMap.pi f = f i
<VAR>R : Type u<VAR>ι : Type x<VAR>Semiring R<VAR>φ : ι → Type i<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<GOAL>⨅ i, LinearMap.ker (LinearMap.proj i) = ⊥
<VAR>R : Type u<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>Semiring R<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>AddCommMonoid M₃<VAR>Module R M₃<VAR>f : M₂ →ₗ[R] M₃<VAR>I : Type u_1<VAR>h : I → M₂<GOAL>∀ (a : I), (f.compLeft I) h a = (⇑f ∘ h) a
<VAR>R : Type u<VAR>M : Type v<VAR>ι : Type x<VAR>Semiring R<VAR>φ : ι → Type i<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>AddCommMonoid M<VAR>Module R M<VAR>DecidableEq ι<VAR>f : (i : ι) → φ i →ₗ[R] M<VAR>i j : ι<VAR>x : φ i<GOAL>(f j) (Pi.single i x j) = Pi.single i ((f i) x) j
<VAR>R : Type u<VAR>ι : Type x<VAR>Semiring R<VAR>φ : ι → Type i<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>DecidableEq ι<VAR>i : ι<GOAL>⇑(LinearMap.single i) = Pi.single i
<VAR>R : Type u<VAR>M : Type v<VAR>ι : Type x<VAR>Semiring R<VAR>φ : ι → Type i<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>S : Type u_1<VAR>AddCommMonoid M<VAR>Module R M<VAR>Fintype ι<VAR>DecidableEq ι<VAR>Semiring S<VAR>Module S M<VAR>SMulCommClass R S M<VAR>f : ((i : ι) → φ i) →ₗ[R] M<VAR>i : ι<GOAL>(LinearMap.lsum R φ S).symm f i = f ∘ₗ LinearMap.single i
<VAR>R : Type u<VAR>M : Type v<VAR>ι : Type x<VAR>Semiring R<VAR>φ : ι → Type i<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>S : Type u_1<VAR>AddCommMonoid M<VAR>Module R M<VAR>Fintype ι<VAR>DecidableEq ι<VAR>Semiring S<VAR>Module S M<VAR>SMulCommClass R S M<VAR>f : (i : ι) → φ i →ₗ[R] M<GOAL>(LinearMap.lsum R φ S) f = ∑ i : ι, f i ∘ₗ LinearMap.proj i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>Fintype ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>M : ι → Type u_3<VAR>(i : ι) → AddCommGroup (M i)<VAR>(i : ι) → Module R (M i)<GOAL>(LinearMap.lsum R M R) LinearMap.single = LinearMap.id
<VAR>R : Type u<VAR>M : Type v<VAR>ι : Type x<VAR>Semiring R<VAR>φ : ι → Type i<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>Finite ι<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>Module R M<VAR>f g : ((i : ι) → φ i) →ₗ[R] M<VAR>h : ∀ (i : ι) (x : φ i), f (Pi.single i x) = g (Pi.single i x)<GOAL>f = g
<VAR>R : Type u<VAR>M : Type v<VAR>ι : Type x<VAR>Semiring R<VAR>φ : ι → Type i<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>Finite ι<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>Module R M<VAR>f g : ((i : ι) → φ i) →ₗ[R] M<GOAL>f = g ↔ ∀ (i : ι) (x : φ i), f (Pi.single i x) = g (Pi.single i x)
<VAR>R : Type u<VAR>M : Type v<VAR>ι : Type x<VAR>Semiring R<VAR>φ : ι → Type i<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>Finite ι<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>Module R M<VAR>f g : ((i : ι) → φ i) →ₗ[R] M<VAR>h : ∀ (i : ι), f ∘ₗ LinearMap.single i = g ∘ₗ LinearMap.single i<GOAL>f = g
<VAR>R : Type u<VAR>M : Type v<VAR>ι : Type x<VAR>Semiring R<VAR>φ : ι → Type i<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>Finite ι<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>Module R M<VAR>f g : ((i : ι) → φ i) →ₗ[R] M<GOAL>f = g ↔ ∀ (i : ι), f ∘ₗ LinearMap.single i = g ∘ₗ LinearMap.single i
<VAR>R : Type u<VAR>M₂ : Type w<VAR>ι : Type x<VAR>Semiring R<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>φ : ι → Type i<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>DecidableEq ι<VAR>f : (i : ι) → M₂ →ₗ[R] φ i<VAR>c : M₂<VAR>i j : ι<VAR>b : M₂ →ₗ[R] φ i<GOAL>(Function.update f i b j) c = Function.update (fun i => (f i) c) i (b c) j
<VAR>R : Type u<VAR>M₂ : Type w<VAR>ι : Type x<VAR>Semiring R<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>Fintype ι<VAR>DecidableEq ι<VAR>f : (ι → R) →ₗ[R] M₂<VAR>x : ι → R<GOAL>f x = ∑ i : ι, x i • f fun j => if i = j then 1 else 0
<VAR>R : Type u<VAR>ι : Type x<VAR>Semiring R<VAR>φ : ι → Type u_1<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>I : Set ι<VAR>p : (i : ι) → Submodule R (φ i)<VAR>x : (i : ι) → φ i<GOAL>x ∈ Submodule.pi I p ↔ ∀ i ∈ I, x i ∈ p i
<VAR>R : Type u<VAR>ι : Type x<VAR>Semiring R<VAR>φ : ι → Type u_1<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>I : Set ι<VAR>p : (i : ι) → Submodule R (φ i)<GOAL>↑(Submodule.pi I p) = I.pi fun i => ↑(p i)
<VAR>R : Type u<VAR>ι : Type x<VAR>Semiring R<VAR>φ : ι → Type u_1<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>p : (i : ι) → Submodule R (φ i)<GOAL>Submodule.pi ∅ p = ⊤
<VAR>R : Type u<VAR>ι : Type x<VAR>Semiring R<VAR>φ : ι → Type u_1<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>s : Set ι<GOAL>(Submodule.pi s fun i => ⊤) = ⊤
<VAR>R : Type u<VAR>ι : Type x<VAR>Semiring R<VAR>φ : ι → Type u_1<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>p q : (i : ι) → Submodule R (φ i)<VAR>s : Set ι<VAR>h : ∀ i ∈ s, p i ≤ q i<GOAL>Submodule.pi s p ≤ Submodule.pi s q
<VAR>R : Type u<VAR>ι : Type x<VAR>Semiring R<VAR>φ : ι → Type u_1<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>I : Set ι<VAR>p : (i : ι) → Submodule R (φ i)<GOAL>⨅ i ∈ I, Submodule.comap (LinearMap.proj i) (p i) = Submodule.pi I p
<VAR>R : Type u<VAR>ι : Type x<VAR>Semiring R<VAR>φ : ι → Type u_1<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>p : (i : ι) → Submodule R (φ i)<GOAL>⨅ i, Submodule.comap (LinearMap.proj i) (p i) = Submodule.pi Set.univ p
<VAR>R : Type u<VAR>ι : Type x<VAR>Semiring R<VAR>φ : ι → Type u_1<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>p : (i : ι) → Submodule R (φ i)<VAR>DecidableEq ι<VAR>Finite ι<GOAL>⨆ i, Submodule.map (LinearMap.single i) (p i) = Submodule.pi Set.univ p
<VAR>R : Type u<VAR>ι : Type x<VAR>Semiring R<VAR>φ : ι → Type u_1<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>DecidableEq ι<VAR>p : (i : ι) → Submodule R (φ i)<VAR>i : ι<GOAL>p i ≤ Submodule.comap (LinearMap.single i) (Submodule.pi Set.univ p)
<VAR>R : Type u<VAR>ι : Type x<VAR>Semiring R<VAR>φ : ι → Type u_1<VAR>ψ : ι → Type u_2<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>(i : ι) → AddCommMonoid (ψ i)<VAR>(i : ι) → Module R (ψ i)<VAR>e : (i : ι) → φ i ≃ₗ[R] ψ i<VAR>f : (i : ι) → φ i<VAR>i : ι<GOAL>(LinearEquiv.piCongrRight e) f i = (e i) (f i)
<VAR>R : Type u<VAR>ι : Type x<VAR>Semiring R<VAR>φ : ι → Type u_1<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<GOAL>(LinearEquiv.piCongrRight fun j => LinearEquiv.refl R (φ j)) = LinearEquiv.refl R ((i : ι) → φ i)
<VAR>R : Type u<VAR>ι : Type x<VAR>Semiring R<VAR>φ : ι → Type u_1<VAR>ψ : ι → Type u_2<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>(i : ι) → AddCommMonoid (ψ i)<VAR>(i : ι) → Module R (ψ i)<VAR>e : (i : ι) → φ i ≃ₗ[R] ψ i<GOAL>(LinearEquiv.piCongrRight e).symm = LinearEquiv.piCongrRight fun i => (e i).symm
<VAR>R : Type u<VAR>ι : Type x<VAR>Semiring R<VAR>φ : ι → Type u_1<VAR>ψ : ι → Type u_2<VAR>χ : ι → Type u_3<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>(i : ι) → AddCommMonoid (ψ i)<VAR>(i : ι) → Module R (ψ i)<VAR>(i : ι) → AddCommMonoid (χ i)<VAR>(i : ι) → Module R (χ i)<VAR>e : (i : ι) → φ i ≃ₗ[R] ψ i<VAR>f : (i : ι) → ψ i ≃ₗ[R] χ i<GOAL>LinearEquiv.piCongrRight e ≪≫ₗ LinearEquiv.piCongrRight f = LinearEquiv.piCongrRight fun i => e i ≪≫ₗ f i
<VAR>R : Type u<VAR>ι : Type x<VAR>ι' : Type x'<VAR>Semiring R<VAR>φ : ι → Type u_1<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>e : ι ≃ ι'<GOAL>∀ (a : (b : ι') → φ (e.symm b)) (a_1 : ι), (LinearEquiv.piCongrLeft' R φ e).symm a a_1 = ⋯ ▸ a (e a_1)
<VAR>R : Type u<VAR>ι : Type x<VAR>ι' : Type x'<VAR>Semiring R<VAR>φ : ι → Type u_1<VAR>(i : ι) → AddCommMonoid (φ i)<VAR>(i : ι) → Module R (φ i)<VAR>e : ι ≃ ι'<GOAL>∀ (a : (a : ι) → φ a) (b : ι'), (LinearEquiv.piCongrLeft' R φ e) a b = a (e.symm b)
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type u_4<VAR>κ : ι → Type u_5<VAR>α : (i : ι) → κ i → Type u_6<VAR>(i : ι) → (k : κ i) → AddCommMonoid (α i k)<VAR>(i : ι) → (k : κ i) → Module R (α i k)<VAR>f : (x : (i : ι) × κ i) → α x.fst x.snd<GOAL>(LinearEquiv.piCurry R α) f = Sigma.curry f
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type u_4<VAR>κ : ι → Type u_5<VAR>α : (i : ι) → κ i → Type u_6<VAR>(i : ι) → (k : κ i) → AddCommMonoid (α i k)<VAR>(i : ι) → (k : κ i) → Module R (α i k)<VAR>f : (a : ι) → (b : κ a) → α a b<GOAL>(LinearEquiv.piCurry R α).symm f = Sigma.uncurry f
<VAR>R : Type u<VAR>M : Type v<VAR>ι : Type x<VAR>Semiring R<VAR>S : Type u_4<VAR>Fintype ι<VAR>DecidableEq ι<VAR>Semiring S<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module S M<VAR>SMulCommClass R S M<VAR>f : (ι → R) →ₗ[R] M<VAR>i : ι<GOAL>(LinearEquiv.piRing R M ι S) f i = f (Pi.single i 1)
<VAR>R : Type u<VAR>M : Type v<VAR>ι : Type x<VAR>Semiring R<VAR>S : Type u_4<VAR>Fintype ι<VAR>DecidableEq ι<VAR>Semiring S<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module S M<VAR>SMulCommClass R S M<VAR>f : ι → M<VAR>g : ι → R<GOAL>((LinearEquiv.piRing R M ι S).symm f) g = ∑ i : ι, g i • f i
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α : Type u_5<VAR>β : Type u_6<VAR>f : α ⊕ β → M<VAR>a : α<GOAL>((LinearEquiv.sumArrowLequivProdArrow α β R M) f).1 a = f (Sum.inl a)
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α : Type u_5<VAR>β : Type u_6<VAR>f : α ⊕ β → M<VAR>b : β<GOAL>((LinearEquiv.sumArrowLequivProdArrow α β R M) f).2 b = f (Sum.inr b)
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α : Type u_5<VAR>β : Type u_6<VAR>f : α → M<VAR>g : β → M<VAR>a : α<GOAL>(LinearEquiv.sumArrowLequivProdArrow α β R M).symm (f, g) (Sum.inl a) = f a
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α : Type u_5<VAR>β : Type u_6<VAR>f : α → M<VAR>g : β → M<VAR>b : β<GOAL>(LinearEquiv.sumArrowLequivProdArrow α β R M).symm (f, g) (Sum.inr b) = g b
<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>M : Type u_7<VAR>Unique ι<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>⇑(LinearEquiv.funUnique ι R M).symm = uniqueElim
<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>M : Type u_7<VAR>Unique ι<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>⇑(LinearEquiv.funUnique ι R M) = Function.eval default
<VAR>R : Type u<VAR>Semiring R<VAR>M : Fin 2 → Type v<VAR>(i : Fin 2) → AddCommMonoid (M i)<VAR>(i : Fin 2) → Module R (M i)<GOAL>⇑(LinearEquiv.piFinTwo R M).symm = fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
<VAR>R : Type u<VAR>Semiring R<VAR>M : Fin 2 → Type v<VAR>(i : Fin 2) → AddCommMonoid (M i)<VAR>(i : Fin 2) → Module R (M i)<GOAL>⇑(LinearEquiv.piFinTwo R M) = fun f => (f 0, f 1)
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>⇑(LinearEquiv.finTwoArrow R M) = fun f => (f 0, f 1)
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>⇑(LinearEquiv.finTwoArrow R M).symm = fun x => ![x.1, x.2]
<VAR>R : Type u<VAR>ι η : Type x<VAR>Semiring R<VAR>s : ι → η<VAR>f : ι → R<GOAL>∀ (a : η), (Function.ExtendByZero.linearMap R s) f a = Function.extend s f 0 a
<VAR>R : Type u<VAR>M : Type v<VAR>M₃ : Type y<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R M₃<VAR>m : M<GOAL>LinearMap.vecEmpty m = ![]
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>n : ℕ<VAR>f : M →ₗ[R] M₂<VAR>g : M →ₗ[R] Fin n → M₂<VAR>m : M<GOAL>(f.vecCons g) m = Matrix.vecCons (f m) (g m)
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<GOAL>∀ (x : M), LinearMap.vecEmpty₂ x = LinearMap.vecEmpty
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>M₃ : Type y<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>n : ℕ<VAR>f : M →ₗ[R] M₂ →ₗ[R] M₃<VAR>g : M →ₗ[R] M₂ →ₗ[R] Fin n → M₃<VAR>m : M<GOAL>(f.vecCons₂ g) m = (f m).vecCons (g m)
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>f : (i : ι) → s i<GOAL>PiTensorProduct.tprodCoeff R 0 f = 0
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>z : R<VAR>f : (i : ι) → s i<VAR>i : ι<VAR>hf : f i = 0<GOAL>PiTensorProduct.tprodCoeff R z f = 0
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>DecidableEq ι<VAR>z : R<VAR>f : (i : ι) → s i<VAR>i : ι<VAR>m₁ m₂ : s i<GOAL>PiTensorProduct.tprodCoeff R z (Function.update f i m₁) + PiTensorProduct.tprodCoeff R z (Function.update f i m₂) = PiTensorProduct.tprodCoeff R z (Function.update f i (m₁ + m₂))
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>z₁ z₂ : R<VAR>f : (i : ι) → s i<GOAL>PiTensorProduct.tprodCoeff R z₁ f + PiTensorProduct.tprodCoeff R z₂ f = PiTensorProduct.tprodCoeff R (z₁ + z₂) f
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>DecidableEq ι<VAR>z : R<VAR>f : (i : ι) → s i<VAR>i : ι<VAR>r : R<GOAL>PiTensorProduct.tprodCoeff R z (Function.update f i (r • f i)) = PiTensorProduct.tprodCoeff R (r * z) f
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>R₁ : Type u_5<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>DecidableEq ι<VAR>z : R<VAR>f : (i : ι) → s i<VAR>i : ι<VAR>r : R₁<VAR>SMul R₁ R<VAR>IsScalarTower R₁ R R<VAR>SMul R₁ (s i)<VAR>IsScalarTower R₁ R (s i)<GOAL>PiTensorProduct.tprodCoeff R z (Function.update f i (r • f i)) = PiTensorProduct.tprodCoeff R (r • z) f
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>motive : (PiTensorProduct R fun i => s i) → Prop<VAR>z : PiTensorProduct R fun i => s i<VAR>tprodCoeff : ∀ (r : R) (f : (i : ι) → s i), motive (PiTensorProduct.tprodCoeff R r f)<VAR>add : ∀ (x y : PiTensorProduct R fun i => s i), motive x → motive y → motive (x + y)<GOAL>motive z
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>R₁ : Type u_5<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>Monoid R₁<VAR>DistribMulAction R₁ R<VAR>SMulCommClass R₁ R R<VAR>r : R₁<VAR>z : R<VAR>f : (i : ι) → s i<GOAL>r • PiTensorProduct.tprodCoeff R z f = PiTensorProduct.tprodCoeff R (r • z) f
<VAR>ι : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>R₁ : Type u_5<VAR>s : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (s i)<VAR>(i : ι) → Module R (s i)<VAR>Monoid R₁<VAR>DistribMulAction R₁ R<VAR>SMulCommClass R₁ R R<VAR>r : R₁<VAR>x y : PiTensorProduct R fun i => s i<GOAL>r • (x + y) = r • x + r • y