ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>f : M → N<VAR>x x' y : M<GOAL>QuadraticMap.polar f (x + x') y = QuadraticMap.polar f x y + QuadraticMap.polar f x' y ↔ f (x + x' + y) + (f x + f x' + f y) = f (x + x') + f (x' + y) + f (y + x)
<VAR>S : Type u_1<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>F : Type u_8<VAR>CommRing S<VAR>FunLike F N S<VAR>AddMonoidHomClass F N S<VAR>f : M → N<VAR>g : F<VAR>x y : M<GOAL>QuadraticMap.polar (⇑g ∘ f) x y = g (QuadraticMap.polar f x y)
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>self : QuadraticMap R M N<VAR>a : R<VAR>x : M<GOAL>self.toFun (a • x) = (a * a) • self.toFun x
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>self : QuadraticMap R M N<GOAL>∃ B, ∀ (x y : M), self.toFun (x + y) = self.toFun x + self.toFun y + (B 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<GOAL>Q.toFun = ⇑Q
<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 Q' : QuadraticMap R M N<VAR>H : ∀ (x : M), Q x = Q' x<GOAL>Q = Q'
<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 Q' : QuadraticMap R M N<VAR>h : Q = Q'<VAR>x : M<GOAL>Q x = Q' 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 Q' : QuadraticMap R M N<GOAL>Q = Q' ↔ ∀ (x : M), Q x = Q' 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>Q' : M → N<VAR>h : Q' = ⇑Q<GOAL>⇑(Q.copy Q' h) = Q'
<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>Q' : M → N<VAR>h : Q' = ⇑Q<GOAL>Q.copy Q' h = Q
<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>a : R<VAR>x : M<GOAL>Q (a • x) = (a * a) • Q 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<GOAL>∃ B, ∀ (x y : M), Q (x + y) = Q x + Q y + (B 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 y z : M<GOAL>Q (x + y + z) + (Q x + Q y + Q z) = Q (x + y) + Q (y + z) + Q (z + 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 (x + x) = 4 • Q 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<GOAL>Q 0 = 0
<VAR>S : Type u_1<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>CommSemiring S<VAR>Algebra S R<VAR>Module S M<VAR>IsScalarTower S R M<VAR>Module S N<VAR>IsScalarTower S R N<VAR>a : S<VAR>x : M<GOAL>Q (a • x) = (a * a) • Q x
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticMap R M N<VAR>x : M<GOAL>Q (-x) = Q x
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticMap R M N<VAR>x y : M<GOAL>Q (x - y) = Q (y - x)
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticMap R M N<VAR>y : M<GOAL>QuadraticMap.polar (⇑Q) 0 y = 0
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticMap R M N<VAR>x x' y : M<GOAL>QuadraticMap.polar (⇑Q) (x + x') y = QuadraticMap.polar (⇑Q) x y + QuadraticMap.polar (⇑Q) x' y
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticMap R M N<VAR>a : R<VAR>x y : M<GOAL>QuadraticMap.polar (⇑Q) (a • x) y = a • QuadraticMap.polar (⇑Q) x y
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticMap R M N<VAR>x y : M<GOAL>QuadraticMap.polar (⇑Q) (-x) y = -QuadraticMap.polar (⇑Q) x y
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticMap R M N<VAR>x x' y : M<GOAL>QuadraticMap.polar (⇑Q) (x - x') y = QuadraticMap.polar (⇑Q) x y - QuadraticMap.polar (⇑Q) x' y
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticMap R M N<VAR>y : M<GOAL>QuadraticMap.polar (⇑Q) y 0 = 0
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticMap R M N<VAR>x y y' : M<GOAL>QuadraticMap.polar (⇑Q) x (y + y') = QuadraticMap.polar (⇑Q) x y + QuadraticMap.polar (⇑Q) x y'
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticMap R M N<VAR>a : R<VAR>x y : M<GOAL>QuadraticMap.polar (⇑Q) x (a • y) = a • QuadraticMap.polar (⇑Q) x y
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticMap R M N<VAR>x y : M<GOAL>QuadraticMap.polar (⇑Q) x (-y) = -QuadraticMap.polar (⇑Q) x y
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticMap R M N<VAR>x y y' : M<GOAL>QuadraticMap.polar (⇑Q) x (y - y') = QuadraticMap.polar (⇑Q) x y - QuadraticMap.polar (⇑Q) x y'
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticMap R M N<VAR>x : M<GOAL>QuadraticMap.polar (⇑Q) x x = 2 • Q x
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticMap R M N<VAR>m y : M<GOAL>(Q.polarBilin m) y = QuadraticMap.polar (⇑Q) m y
<VAR>S : Type u_1<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticMap R M N<VAR>CommSemiring S<VAR>Algebra S R<VAR>Module S M<VAR>IsScalarTower S R M<VAR>Module S N<VAR>IsScalarTower S R N<VAR>a : S<VAR>x y : M<GOAL>QuadraticMap.polar (⇑Q) (a • x) y = a • QuadraticMap.polar (⇑Q) x y
<VAR>S : Type u_1<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticMap R M N<VAR>CommSemiring S<VAR>Algebra S R<VAR>Module S M<VAR>IsScalarTower S R M<VAR>Module S N<VAR>IsScalarTower S R N<VAR>a : S<VAR>x y : M<GOAL>QuadraticMap.polar (⇑Q) x (a • y) = a • QuadraticMap.polar (⇑Q) x y
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>toFun : M → N<VAR>toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x<VAR>polar_add_left : ∀ (x x' y : M), QuadraticMap.polar toFun (x + x') y = QuadraticMap.polar toFun x y + QuadraticMap.polar toFun x' y<VAR>polar_smul_left : ∀ (a : R) (x y : M), QuadraticMap.polar toFun (a • x) y = a • QuadraticMap.polar toFun x y<GOAL>∀ (a : M), (QuadraticMap.ofPolar toFun toFun_smul polar_add_left polar_smul_left) a = toFun a
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticMap R M N<GOAL>⋯.choose = Q.polarBilin
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>ι : Type u_8<VAR>DecidableEq ι<VAR>Q : QuadraticMap R M N<VAR>s : Finset ι<VAR>f : ι → M<GOAL>Q (∑ i ∈ s, f i) = ∑ i ∈ s, Q (f i) + ∑ ij ∈ Finset.filter (fun x => ¬x.IsDiag) s.sym2, Sym2.lift ⟨fun i j => QuadraticMap.polar (⇑Q) (f i) (f j), ⋯⟩ ij
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>ι : Type u_8<VAR>Q : QuadraticMap R M N<VAR>s : Finset ι<VAR>f : ι → M<GOAL>Q (∑ i ∈ s, f i) = ∑ ij ∈ s.sym2, Sym2.lift ⟨fun i j => QuadraticMap.polar (⇑Q) (f i) (f j), ⋯⟩ ij - ∑ i ∈ s, Q (f i)
<VAR>S : Type u_1<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>Monoid S<VAR>DistribMulAction S N<VAR>SMulCommClass S R N<VAR>a : S<VAR>Q : QuadraticMap R M N<GOAL>⇑(a • Q) = a • ⇑Q
<VAR>S : Type u_1<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>Monoid S<VAR>DistribMulAction S N<VAR>SMulCommClass S R N<VAR>a : S<VAR>Q : QuadraticMap R M N<VAR>x : M<GOAL>(a • Q) x = a • Q 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<GOAL>⇑0 = 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>x : M<GOAL>0 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 Q' : QuadraticMap R M N<GOAL>⇑(Q + Q') = ⇑Q + ⇑Q'
<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 Q' : QuadraticMap R M N<VAR>x : M<GOAL>(Q + Q') x = Q x + Q' 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<GOAL>∀ (a : QuadraticMap R M N) (a_1 : M), QuadraticMap.coeFnAddMonoidHom a a_1 = a a_1
<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>m : M<GOAL>∀ (a : QuadraticMap R M N), (QuadraticMap.evalAddMonoidHom m) a = a m
<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>Q : ι → QuadraticMap R M N<VAR>s : Finset ι<GOAL>⇑(∑ i ∈ s, Q i) = ∑ i ∈ s, ⇑(Q i)
<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>Q : ι → QuadraticMap R M N<VAR>s : Finset ι<VAR>x : M<GOAL>(∑ i ∈ s, Q i) x = ∑ i ∈ s, (Q i) x
<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<GOAL>⇑(-Q) = -⇑Q
<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 : M<GOAL>(-Q) x = -Q x
<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 Q' : QuadraticMap R M N<GOAL>⇑(Q - Q') = ⇑Q - ⇑Q'
<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 Q' : QuadraticMap R M N<VAR>x : M<GOAL>(Q - Q') x = Q x - Q' x
<VAR>S : Type u_1<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommSemiring R<VAR>CommSemiring S<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>Module S M<VAR>Module S N<VAR>Algebra S R<VAR>IsScalarTower S R M<VAR>IsScalarTower S R N<VAR>Q : QuadraticMap R M N<VAR>x : M<GOAL>Q.restrictScalars x = Q x
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>AddCommMonoid P<VAR>Module R P<VAR>Q : QuadraticMap R N P<VAR>f : M →ₗ[R] N<VAR>x : M<GOAL>(Q.comp f) x = Q (f x)
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>AddCommMonoid P<VAR>Module R P<VAR>f : N →ₗ[R] P<VAR>Q : QuadraticMap R M N<VAR>x : M<GOAL>(f.compQuadraticMap Q) x = f (Q x)
<VAR>S : Type u_1<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>AddCommMonoid P<VAR>CommSemiring S<VAR>Algebra S R<VAR>Module S N<VAR>Module S M<VAR>IsScalarTower S R N<VAR>IsScalarTower S R M<VAR>Module S P<VAR>f : N →ₗ[S] P<VAR>Q : QuadraticMap R M N<VAR>x : M<GOAL>(f.compQuadraticMap' Q) x = f (Q x)
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>A : Type u_7<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>f g : M →ₗ[R] A<VAR>x : M<GOAL>(QuadraticMap.linMulLin f g) x = f x * g x
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>A : Type u_7<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>f g h : M →ₗ[R] A<GOAL>QuadraticMap.linMulLin (f + g) h = QuadraticMap.linMulLin f h + QuadraticMap.linMulLin g h
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>A : Type u_7<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>f g h : M →ₗ[R] A<GOAL>QuadraticMap.linMulLin f (g + h) = QuadraticMap.linMulLin f g + QuadraticMap.linMulLin f h
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>A : Type u_7<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>N' : Type u_8<VAR>AddCommMonoid N'<VAR>Module R N'<VAR>f g : M →ₗ[R] A<VAR>h : N' →ₗ[R] M<GOAL>(QuadraticMap.linMulLin f g).comp h = QuadraticMap.linMulLin (f ∘ₗ h) (g ∘ₗ h)
<VAR>R : Type u_3<VAR>A : Type u_7<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>a : A<GOAL>QuadraticMap.sq a = a * a
<VAR>R : Type u_3<VAR>A : Type u_7<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>n : Type u_9<VAR>i j : n<VAR>x : n → A<GOAL>(QuadraticMap.proj i j) x = x i * x j
<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>B : LinearMap.BilinMap R M N<VAR>x : M<GOAL>B.toQuadraticMap x = (B x) 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>N' : Type u_8<VAR>AddCommMonoid N'<VAR>Module R N'<VAR>B : LinearMap.BilinMap R M N<VAR>f : N' →ₗ[R] M<GOAL>LinearMap.BilinMap.toQuadraticMap (LinearMap.compl₁₂ B f f) = B.toQuadraticMap.comp f
<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<GOAL>LinearMap.BilinMap.toQuadraticMap 0 = 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>B₁ B₂ : LinearMap.BilinMap R M N<GOAL>(B₁ + B₂).toQuadraticMap = B₁.toQuadraticMap + B₂.toQuadraticMap
<VAR>S : Type u_1<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>Monoid S<VAR>DistribMulAction S N<VAR>SMulCommClass S R N<VAR>SMulCommClass R S N<VAR>a : S<VAR>B : LinearMap.BilinMap R M N<GOAL>(a • B).toQuadraticMap = a • B.toQuadraticMap
<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>B : LinearMap.BilinMap R M N<GOAL>(LinearMap.BilinMap.toQuadraticMapAddMonoidHom R M) B = B.toQuadraticMap
<VAR>S : Type u_1<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>Semiring S<VAR>Module S N<VAR>SMulCommClass S R N<VAR>SMulCommClass R S N<VAR>B : LinearMap.BilinMap R M N<VAR>x : M<GOAL>((LinearMap.BilinMap.toQuadraticMapLinearMap S R M) B) x = (B x) 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>B : List (LinearMap.BilinMap R M N)<GOAL>B.sum.toQuadraticMap = (List.map LinearMap.BilinMap.toQuadraticMap B).sum
<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>B : Multiset (LinearMap.BilinMap R M N)<GOAL>B.sum.toQuadraticMap = (Multiset.map LinearMap.BilinMap.toQuadraticMap B).sum
<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_9<VAR>s : Finset ι<VAR>B : ι → LinearMap.BilinMap R M N<GOAL>(∑ i ∈ s, B i).toQuadraticMap = ∑ i ∈ s, (B i).toQuadraticMap
<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>B : LinearMap.BilinMap R M N<GOAL>B.toQuadraticMap = 0 ↔ LinearMap.IsAlt B
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>B : LinearMap.BilinMap R M N<GOAL>(-B).toQuadraticMap = -B.toQuadraticMap
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>B₁ B₂ : LinearMap.BilinMap R M N<GOAL>(B₁ - B₂).toQuadraticMap = B₁.toQuadraticMap - B₂.toQuadraticMap
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>B : LinearMap.BilinMap R M N<VAR>x y : M<GOAL>QuadraticMap.polar (⇑B.toQuadraticMap) x y = (B x) y + (B y) x
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>B : LinearMap.BilinMap R M N<GOAL>B.toQuadraticMap.polarBilin = B + LinearMap.flip B
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticMap R M N<GOAL>Q.polarBilin.toQuadraticMap = 2 • Q
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>h : IsUnit 2<GOAL>Function.Injective QuadraticMap.polarBilin
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>N' : Type u_8<VAR>AddCommGroup N'<VAR>Module R N'<VAR>Q : QuadraticMap R N' N<VAR>f : M →ₗ[R] N'<GOAL>(Q.comp f).polarBilin = LinearMap.compl₁₂ Q.polarBilin f f
<VAR>S : Type u_1<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>N' : Type u_8<VAR>AddCommGroup N'<VAR>CommSemiring S<VAR>Algebra S R<VAR>Module S N<VAR>Module S N'<VAR>IsScalarTower S R N<VAR>Module S M<VAR>IsScalarTower S R M<VAR>f : N →ₗ[S] N'<VAR>Q : QuadraticMap R M N<VAR>x y : M<GOAL>QuadraticMap.polar (⇑(f.compQuadraticMap' Q)) x y = f (QuadraticMap.polar (⇑Q) x y)
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>N' : Type u_8<VAR>AddCommGroup N'<VAR>Module R N'<VAR>f : N →ₗ[R] N'<VAR>Q : QuadraticMap R M N<GOAL>(f.compQuadraticMap' Q).polarBilin = LinearMap.compr₂ Q.polarBilin f
<VAR>S : Type u_1<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>CommSemiring S<VAR>Algebra S R<VAR>Module S N<VAR>IsScalarTower S R N<VAR>Invertible 2<VAR>Q : QuadraticMap R M N<VAR>x y : M<GOAL>(((QuadraticMap.associatedHom S) Q) x) y = ⅟2 • (Q (x + y) - Q x - Q y)
<VAR>S : Type u_1<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>CommSemiring S<VAR>Algebra S R<VAR>Module S N<VAR>IsScalarTower S R N<VAR>Invertible 2<VAR>Q : QuadraticMap R M N<GOAL>2 • (QuadraticMap.associatedHom S) Q = Q.polarBilin
<VAR>S : Type u_1<VAR>R : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>CommSemiring S<VAR>Algebra S R<VAR>Invertible 2<VAR>Q : QuadraticMap R M R<GOAL>LinearMap.IsSymm ((QuadraticMap.associatedHom S) Q)
<VAR>S : Type u_1<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>CommSemiring S<VAR>Algebra S R<VAR>Module S N<VAR>IsScalarTower S R N<VAR>Invertible 2<VAR>Q : QuadraticMap R M N<VAR>N' : Type u_8<VAR>AddCommGroup N'<VAR>Module R N'<VAR>f : N' →ₗ[R] M<GOAL>(QuadraticMap.associatedHom S) (Q.comp f) = LinearMap.compl₁₂ ((QuadraticMap.associatedHom S) Q) f f
<VAR>S : Type u_1<VAR>R : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>CommSemiring S<VAR>Algebra S R<VAR>Invertible 2<VAR>B : LinearMap.BilinMap R M R<VAR>x y : M<GOAL>(((QuadraticMap.associatedHom S) B.toQuadraticMap) x) y = ⅟2 • ((B x) y + (B y) x)
<VAR>S : Type u_1<VAR>R : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>CommSemiring S<VAR>Algebra S R<VAR>Invertible 2<VAR>B₁ : LinearMap.BilinMap R M R<VAR>h : LinearMap.IsSymm B₁<GOAL>(QuadraticMap.associatedHom S) B₁.toQuadraticMap = B₁
<VAR>S : Type u_1<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>CommSemiring S<VAR>Algebra S R<VAR>Module S N<VAR>IsScalarTower S R N<VAR>Invertible 2<VAR>Q : QuadraticMap R M N<VAR>x : M<GOAL>(((QuadraticMap.associatedHom S) Q) x) x = Q x
<VAR>S : Type u_1<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>CommSemiring S<VAR>Algebra S R<VAR>Module S N<VAR>IsScalarTower S R N<VAR>Invertible 2<VAR>Q : QuadraticMap R M N<GOAL>((QuadraticMap.associatedHom S) Q).toQuadraticMap = Q
<VAR>S : Type u_1<VAR>R : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>CommSemiring S<VAR>Algebra S R<VAR>Invertible 2<GOAL>Function.RightInverse (⇑(QuadraticMap.associatedHom S)) LinearMap.BilinMap.toQuadraticMap
<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 : QuadraticForm R M<VAR>hB₁ : QuadraticMap.associated' Q ≠ 0<GOAL>∃ x, Q x ≠ 0
<VAR>S : Type u_1<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommSemiring S<VAR>CommRing R<VAR>AddCommGroup M<VAR>Algebra S R<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>Module S N<VAR>IsScalarTower S R N<VAR>Invertible 2<GOAL>⇑(QuadraticMap.associatedHom S) = ⇑QuadraticMap.associated
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Invertible 2<VAR>f g : M →ₗ[R] R<GOAL>QuadraticMap.associated (QuadraticMap.linMulLin f g) = ⅟2 • ((LinearMap.mul R R).compl₁₂ f g + (LinearMap.mul R R).compl₁₂ g f)
<VAR>R : Type u_3<VAR>CommRing R<VAR>Invertible 2<GOAL>QuadraticMap.associated QuadraticMap.sq = LinearMap.mul R R