ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R₁ : Type u_4<VAR>M₁ : Type u_5<VAR>CommRing R₁<VAR>AddCommGroup M₁<VAR>Module R₁ M₁<VAR>B₁ : LinearMap.BilinForm R₁ M₁<VAR>x y : M₁<GOAL>(B₁ x) (-y) = -(B₁ x) y
<VAR>R₁ : Type u_4<VAR>M₁ : Type u_5<VAR>CommRing R₁<VAR>AddCommGroup M₁<VAR>Module R₁ M₁<VAR>B₁ : LinearMap.BilinForm R₁ M₁<VAR>x y z : M₁<GOAL>(B₁ (x - y)) z = (B₁ x) z - (B₁ y) z
<VAR>R₁ : Type u_4<VAR>M₁ : Type u_5<VAR>CommRing R₁<VAR>AddCommGroup M₁<VAR>Module R₁ M₁<VAR>B₁ : LinearMap.BilinForm R₁ M₁<VAR>x y z : M₁<GOAL>(B₁ x) (y - z) = (B₁ x) y - (B₁ x) z
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Type u_3<VAR>CommSemiring S<VAR>Algebra S R<VAR>Module S M<VAR>IsScalarTower S R M<VAR>B : LinearMap.BilinForm R M<VAR>r : S<VAR>x y : M<GOAL>(B (r • x)) y = r • (B x) y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Type u_3<VAR>CommSemiring S<VAR>Algebra S R<VAR>Module S M<VAR>IsScalarTower S R M<VAR>B : LinearMap.BilinForm R M<VAR>r : S<VAR>x y : M<GOAL>(B x) (r • y) = r • (B x) y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Function.Injective fun B x y => (B x) y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B D : LinearMap.BilinForm R M<VAR>H : ∀ (x y : M), (B x) y = (D x) y<GOAL>B = D
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B D : LinearMap.BilinForm R M<VAR>h : B = D<VAR>x y : M<GOAL>(B x) y = (D x) y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B D : LinearMap.BilinForm R M<GOAL>B = D ↔ ∀ (x y : M), (B x) y = (D x) y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>⇑0 = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x y : M<GOAL>(0 x) y = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B D : LinearMap.BilinForm R M<GOAL>⇑(B + D) = ⇑B + ⇑D
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B D : LinearMap.BilinForm R M<VAR>x y : M<GOAL>((B + D) x) y = (B x) y + (D x) y
<VAR>R₁ : Type u_4<VAR>M₁ : Type u_5<VAR>CommRing R₁<VAR>AddCommGroup M₁<VAR>Module R₁ M₁<VAR>B₁ : LinearMap.BilinForm R₁ M₁<GOAL>⇑(-B₁) = -⇑B₁
<VAR>R₁ : Type u_4<VAR>M₁ : Type u_5<VAR>CommRing R₁<VAR>AddCommGroup M₁<VAR>Module R₁ M₁<VAR>B₁ : LinearMap.BilinForm R₁ M₁<VAR>x y : M₁<GOAL>((-B₁) x) y = -(B₁ x) y
<VAR>R₁ : Type u_4<VAR>M₁ : Type u_5<VAR>CommRing R₁<VAR>AddCommGroup M₁<VAR>Module R₁ M₁<VAR>B₁ D₁ : LinearMap.BilinForm R₁ M₁<GOAL>⇑(B₁ - D₁) = ⇑B₁ - ⇑D₁
<VAR>R₁ : Type u_4<VAR>M₁ : Type u_5<VAR>CommRing R₁<VAR>AddCommGroup M₁<VAR>Module R₁ M₁<VAR>B₁ D₁ : LinearMap.BilinForm R₁ M₁<VAR>x y : M₁<GOAL>((B₁ - D₁) x) y = (B₁ x) y - (D₁ x) y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>A : LinearMap.BilinForm R M<GOAL>LinearMap.BilinForm.flipHomAux (LinearMap.BilinForm.flipHomAux A) = A
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>A : LinearMap.BilinForm R M<VAR>x y : M<GOAL>((LinearMap.BilinForm.flipHom A) x) y = (A y) x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>LinearMap.BilinForm.flipHom ≪≫ₗ LinearMap.BilinForm.flipHom = LinearEquiv.refl R (LinearMap.BilinForm R M)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>W : Submodule R M<VAR>m : ↥W<GOAL>(B.restrict W) m = (B ↑m).domRestrict W
<VAR>R : Type u<VAR>CommRing R<VAR>Invertible 2<VAR>X Y : QuadraticModuleCat R<GOAL>(QuadraticModuleCat.instMonoidalCategory.tensorObj X Y).form = X.form.tmul Y.form
<VAR>R : Type u<VAR>CommRing R<VAR>Invertible 2<VAR>X Y : QuadraticModuleCat R<GOAL>(X ⊗ Y).toModuleCat = X.toModuleCat ⊗ Y.toModuleCat
<VAR>R : Type u<VAR>CommRing R<VAR>Invertible 2<VAR>X Y Z : QuadraticModuleCat R<GOAL>(CategoryTheory.forget₂ (QuadraticModuleCat R) (ModuleCat R)).map (α_ X Y Z).hom = (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat).hom
<VAR>R : Type u<VAR>CommRing R<VAR>Invertible 2<VAR>X Y Z : QuadraticModuleCat R<GOAL>(CategoryTheory.forget₂ (QuadraticModuleCat R) (ModuleCat R)).map (α_ X Y Z).inv = (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat).inv
<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>P : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid P<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R P<VAR>Q₁ : QuadraticMap R M₁ P<VAR>Q₂ : QuadraticMap R M₂ P<VAR>a : M₁ × M₂<GOAL>(Q₁.prod Q₂) a = Q₁ a.1 + Q₂ a.2
<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>P : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid N₁<VAR>AddCommMonoid N₂<VAR>AddCommMonoid P<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R N₁<VAR>Module R N₂<VAR>Module R P<VAR>Q₁ : QuadraticMap R M₁ P<VAR>Q₂ : QuadraticMap R M₂ P<VAR>Q₁' : QuadraticMap R N₁ P<VAR>Q₂' : QuadraticMap R N₂ P<VAR>e₁ : Q₁.IsometryEquiv Q₁'<VAR>e₂ : Q₂.IsometryEquiv Q₂'<GOAL>(e₁.prod e₂).toLinearEquiv = e₁.prod e₂.toLinearEquiv
<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>P : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid P<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R P<VAR>Q₁ : QuadraticMap R M₁ P<VAR>Q₂ : QuadraticMap R M₂ P<VAR>i : M₁<GOAL>(QuadraticMap.Isometry.inl Q₁ Q₂) i = (i, 0)
<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>P : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid P<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R P<VAR>Q₁ : QuadraticMap R M₁ P<VAR>Q₂ : QuadraticMap R M₂ P<VAR>i : M₂<GOAL>(QuadraticMap.Isometry.inr Q₁ Q₂) i = (0, i)
<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>P : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid P<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R P<VAR>Q₁ : QuadraticMap R M₁ P<VAR>self : M₁ × M₂<GOAL>(QuadraticMap.Isometry.fst M₂ Q₁) self = self.1
<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>P : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid P<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R P<VAR>Q₂ : QuadraticMap R M₂ P<VAR>self : M₁ × M₂<GOAL>(QuadraticMap.Isometry.snd M₁ Q₂) self = self.2
<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>P : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid P<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R P<VAR>Q₁ : QuadraticMap R M₁ P<GOAL>(QuadraticMap.Isometry.fst M₂ Q₁).comp (QuadraticMap.Isometry.inl Q₁ 0) = QuadraticMap.Isometry.id Q₁
<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>P : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid P<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R P<VAR>Q₂ : QuadraticMap R M₂ P<GOAL>(QuadraticMap.Isometry.snd M₁ Q₂).comp (QuadraticMap.Isometry.inr 0 Q₂) = QuadraticMap.Isometry.id Q₂
<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>P : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid P<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R P<VAR>Q₂ : QuadraticMap R M₂ P<GOAL>(QuadraticMap.Isometry.snd M₁ Q₂).comp (QuadraticMap.Isometry.inl 0 Q₂) = 0
<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>P : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid P<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R P<VAR>Q₁ : QuadraticMap R M₁ P<GOAL>(QuadraticMap.Isometry.fst M₂ Q₁).comp (QuadraticMap.Isometry.inr Q₁ 0) = 0
<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>P : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid N₁<VAR>AddCommMonoid N₂<VAR>AddCommMonoid P<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R N₁<VAR>Module R N₂<VAR>Module R P<VAR>Q₁ : QuadraticMap R M₁ P<VAR>Q₂ : QuadraticMap R M₂ P<VAR>Q₁' : QuadraticMap R N₁ P<VAR>Q₂' : QuadraticMap R N₂ P<VAR>e₁ : Q₁.Equivalent Q₁'<VAR>e₂ : Q₂.Equivalent Q₂'<GOAL>(Q₁.prod Q₂).Equivalent (Q₁'.prod Q₂')
<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>P : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid P<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R P<VAR>Q₁ : QuadraticMap R M₁ P<VAR>Q₂ : QuadraticMap R M₂ P<GOAL>∀ (a : M₂ × M₁), (QuadraticMap.IsometryEquiv.prodComm Q₁ Q₂).invFun a = a.swap
<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>P : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid P<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R P<VAR>Q₁ : QuadraticMap R M₁ P<VAR>Q₂ : QuadraticMap R M₂ P<GOAL>∀ (a : M₁ × M₂), (QuadraticMap.IsometryEquiv.prodComm Q₁ Q₂) a = a.swap
<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>P : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid N₁<VAR>AddCommMonoid N₂<VAR>AddCommMonoid P<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R N₁<VAR>Module R N₂<VAR>Module R P<VAR>Q₁ : QuadraticMap R M₁ P<VAR>Q₂ : QuadraticMap R M₂ P<VAR>Q₃ : QuadraticMap R N₁ P<VAR>Q₄ : QuadraticMap R N₂ P<VAR>mmnn : (M₁ × N₁) × M₂ × N₂<GOAL>(QuadraticMap.IsometryEquiv.prodProdProdComm Q₁ Q₂ Q₃ Q₄).invFun mmnn = ((mmnn.1.1, mmnn.2.1), mmnn.1.2, mmnn.2.2)
<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>P : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid N₁<VAR>AddCommMonoid N₂<VAR>AddCommMonoid P<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R N₁<VAR>Module R N₂<VAR>Module R P<VAR>Q₁ : QuadraticMap R M₁ P<VAR>Q₂ : QuadraticMap R M₂ P<VAR>Q₃ : QuadraticMap R N₁ P<VAR>Q₄ : QuadraticMap R N₂ P<VAR>mnmn : (M₁ × M₂) × N₁ × N₂<GOAL>(QuadraticMap.IsometryEquiv.prodProdProdComm Q₁ Q₂ Q₃ Q₄) mnmn = ((mnmn.1.1, mnmn.2.1), mnmn.1.2, mnmn.2.2)
<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>P : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid P<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R P<VAR>Q₁ : QuadraticMap R M₁ P<VAR>Q₂ : QuadraticMap R M₂ P<VAR>h : (Q₁.prod Q₂).Anisotropic<GOAL>Q₁.Anisotropic ∧ Q₂.Anisotropic
<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>P : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid P<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R P<VAR>Preorder P<VAR>CovariantClass P P (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Q₁ : QuadraticMap R M₁ P<VAR>Q₂ : QuadraticMap R M₂ P<GOAL>(∀ (x : M₁ × M₂), 0 ≤ (Q₁.prod Q₂) x) ↔ (∀ (x : M₁), 0 ≤ Q₁ x) ∧ ∀ (x : M₂), 0 ≤ Q₂ x
<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>P : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid P<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R P<VAR>PartialOrder P<VAR>CovariantClass P P (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Q₁ : QuadraticMap R M₁ P<VAR>Q₂ : QuadraticMap R M₂ P<GOAL>(Q₁.prod Q₂).PosDef ↔ Q₁.PosDef ∧ Q₂.PosDef
<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>P : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid P<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R P<VAR>PartialOrder P<VAR>CovariantClass P P (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Q₁ : QuadraticMap R M₁ P<VAR>Q₂ : QuadraticMap R M₂ P<VAR>h₁ : Q₁.PosDef<VAR>h₂ : Q₂.PosDef<GOAL>(Q₁.prod Q₂).PosDef
<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>P : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid P<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R P<VAR>Q₁ : QuadraticMap R M₁ P<VAR>Q₂ : QuadraticMap R M₂ P<VAR>v w : M₁ × M₂<VAR>h₁ : Q₁.IsOrtho v.1 w.1<VAR>h₂ : Q₂.IsOrtho v.2 w.2<GOAL>(Q₁.prod Q₂).IsOrtho v w
<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>P : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid P<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R P<VAR>Q₁ : QuadraticMap R M₁ P<VAR>Q₂ : QuadraticMap R M₂ P<VAR>m₁ : M₁<VAR>m₂ : M₂<GOAL>(Q₁.prod Q₂).IsOrtho (m₁, 0) (0, m₂)
<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>P : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid P<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R P<VAR>Q₁ : QuadraticMap R M₁ P<VAR>Q₂ : QuadraticMap R M₂ P<VAR>m₁ : M₁<VAR>m₂ : M₂<GOAL>(Q₁.prod Q₂).IsOrtho (0, m₂) (m₁, 0)
<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>P : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid P<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R P<VAR>Q₁ : QuadraticMap R M₁ P<VAR>Q₂ : QuadraticMap R M₂ P<VAR>m₁ m₁' : M₁<GOAL>(Q₁.prod Q₂).IsOrtho (m₁, 0) (m₁', 0) ↔ Q₁.IsOrtho m₁ m₁'
<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>P : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid P<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R P<VAR>Q₁ : QuadraticMap R M₁ P<VAR>Q₂ : QuadraticMap R M₂ P<VAR>m₂ m₂' : M₂<GOAL>(Q₁.prod Q₂).IsOrtho (0, m₂) (0, m₂') ↔ Q₂.IsOrtho m₂ m₂'
<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>P : Type u_7<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>AddCommGroup P<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R P<VAR>Q₁ : QuadraticMap R M₁ P<VAR>Q₂ : QuadraticMap R M₂ P<VAR>x y : M₁ × M₂<GOAL>QuadraticMap.polar (⇑(Q₁.prod Q₂)) x y = QuadraticMap.polar (⇑Q₁) x.1 y.1 + QuadraticMap.polar (⇑Q₂) x.2 y.2
<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>P : Type u_7<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>AddCommGroup P<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R P<VAR>Q₁ : QuadraticMap R M₁ P<VAR>Q₂ : QuadraticMap R M₂ P<GOAL>(Q₁.prod Q₂).polarBilin = LinearMap.compl₁₂ Q₁.polarBilin (LinearMap.fst R M₁ M₂) (LinearMap.fst R M₁ M₂) + LinearMap.compl₁₂ Q₂.polarBilin (LinearMap.snd R M₁ M₂) (LinearMap.snd R M₁ M₂)
<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>P : Type u_7<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>AddCommGroup P<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R P<VAR>Invertible 2<VAR>Q₁ : QuadraticMap R M₁ P<VAR>Q₂ : QuadraticMap R M₂ P<GOAL>QuadraticMap.associated (Q₁.prod Q₂) = LinearMap.compl₁₂ (QuadraticMap.associated Q₁) (LinearMap.fst R M₁ M₂) (LinearMap.fst R M₁ M₂) + LinearMap.compl₁₂ (QuadraticMap.associated Q₂) (LinearMap.snd R M₁ M₂) (LinearMap.snd R M₁ M₂)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>P : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (Mᵢ i)<VAR>AddCommMonoid P<VAR>(i : ι) → Module R (Mᵢ i)<VAR>Module R P<VAR>Fintype ι<VAR>Q : (i : ι) → QuadraticMap R (Mᵢ i) P<VAR>x : (i : ι) → Mᵢ i<GOAL>(QuadraticMap.pi Q) x = ∑ i : ι, (Q i) (x i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>P : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (Mᵢ i)<VAR>AddCommMonoid P<VAR>(i : ι) → Module R (Mᵢ i)<VAR>Module R P<VAR>Fintype ι<VAR>DecidableEq ι<VAR>Q : (i : ι) → QuadraticMap R (Mᵢ i) P<VAR>i : ι<VAR>m : Mᵢ i<GOAL>(QuadraticMap.pi Q) (Pi.single i m) = (Q i) m
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>P : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>Nᵢ : ι → Type u_9<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (Mᵢ i)<VAR>(i : ι) → AddCommMonoid (Nᵢ i)<VAR>AddCommMonoid P<VAR>(i : ι) → Module R (Mᵢ i)<VAR>(i : ι) → Module R (Nᵢ i)<VAR>Module R P<VAR>Fintype ι<VAR>Q : (i : ι) → QuadraticMap R (Mᵢ i) P<VAR>Q' : (i : ι) → QuadraticMap R (Nᵢ i) P<VAR>e : (i : ι) → (Q i).IsometryEquiv (Q' i)<GOAL>(QuadraticMap.IsometryEquiv.pi e).toLinearEquiv = LinearEquiv.piCongrRight fun i => (e i).toLinearEquiv
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>P : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (Mᵢ i)<VAR>AddCommMonoid P<VAR>(i : ι) → Module R (Mᵢ i)<VAR>Module R P<VAR>Fintype ι<VAR>DecidableEq ι<VAR>Q : (i : ι) → QuadraticMap R (Mᵢ i) P<VAR>i : ι<VAR>x : Mᵢ i<VAR>j : ι<GOAL>(QuadraticMap.Isometry.single Q i) x j = Pi.single i x j
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>P : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (Mᵢ i)<VAR>AddCommMonoid P<VAR>(i : ι) → Module R (Mᵢ i)<VAR>Module R P<VAR>Fintype ι<VAR>DecidableEq ι<VAR>i : ι<VAR>Q : QuadraticMap R (Mᵢ i) P<VAR>f : (x : ι) → Mᵢ x<GOAL>(QuadraticMap.Isometry.proj i Q) f = f i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>P : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (Mᵢ i)<VAR>AddCommMonoid P<VAR>(i : ι) → Module R (Mᵢ i)<VAR>Module R P<VAR>Fintype ι<VAR>DecidableEq ι<VAR>i : ι<VAR>Q : QuadraticMap R (Mᵢ i) P<GOAL>(QuadraticMap.Isometry.proj i Q).comp (QuadraticMap.Isometry.single (Pi.single i Q) i) = QuadraticMap.Isometry.ofEq ⋯
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>P : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (Mᵢ i)<VAR>AddCommMonoid P<VAR>(i : ι) → Module R (Mᵢ i)<VAR>Module R P<VAR>Fintype ι<VAR>DecidableEq ι<VAR>i j : ι<VAR>h : i ≠ j<VAR>Q : QuadraticMap R (Mᵢ i) P<GOAL>(QuadraticMap.Isometry.proj i Q).comp (QuadraticMap.Isometry.single (Pi.single i Q) j) = QuadraticMap.Isometry.comp 0 (QuadraticMap.Isometry.ofEq ⋯)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>P : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>Nᵢ : ι → Type u_9<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (Mᵢ i)<VAR>(i : ι) → AddCommMonoid (Nᵢ i)<VAR>AddCommMonoid P<VAR>(i : ι) → Module R (Mᵢ i)<VAR>(i : ι) → Module R (Nᵢ i)<VAR>Module R P<VAR>Fintype ι<VAR>Q : (i : ι) → QuadraticMap R (Mᵢ i) P<VAR>Q' : (i : ι) → QuadraticMap R (Nᵢ i) P<VAR>e : ∀ (i : ι), (Q i).Equivalent (Q' i)<GOAL>(QuadraticMap.pi Q).Equivalent (QuadraticMap.pi Q')
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>P : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (Mᵢ i)<VAR>AddCommMonoid P<VAR>(i : ι) → Module R (Mᵢ i)<VAR>Module R P<VAR>Fintype ι<VAR>Q : (i : ι) → QuadraticMap R (Mᵢ i) P<VAR>h : (QuadraticMap.pi Q).Anisotropic<VAR>i : ι<GOAL>(Q i).Anisotropic
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>Mᵢ : ι → Type u_8<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (Mᵢ i)<VAR>(i : ι) → Module R (Mᵢ i)<VAR>P : Type u_10<VAR>Fintype ι<VAR>OrderedAddCommMonoid P<VAR>Module R P<VAR>Q : (i : ι) → QuadraticMap R (Mᵢ i) P<GOAL>(∀ (x : (i : ι) → Mᵢ i), 0 ≤ (QuadraticMap.pi Q) x) ↔ ∀ (i : ι) (x : Mᵢ i), 0 ≤ (Q i) x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>Mᵢ : ι → Type u_8<VAR>CommSemiring R<VAR>(i : ι) → AddCommMonoid (Mᵢ i)<VAR>(i : ι) → Module R (Mᵢ i)<VAR>P : Type u_10<VAR>Fintype ι<VAR>OrderedAddCommMonoid P<VAR>Module R P<VAR>Q : (i : ι) → QuadraticMap R (Mᵢ i) P<GOAL>(QuadraticMap.pi Q).PosDef ↔ ∀ (i : ι), (Q i).PosDef
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>P : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>CommRing R<VAR>(i : ι) → AddCommGroup (Mᵢ i)<VAR>AddCommGroup P<VAR>(i : ι) → Module R (Mᵢ i)<VAR>Module R P<VAR>Fintype ι<VAR>Q : (i : ι) → QuadraticMap R (Mᵢ i) P<VAR>x y : (i : ι) → Mᵢ i<GOAL>QuadraticMap.polar (⇑(QuadraticMap.pi Q)) x y = ∑ i : ι, QuadraticMap.polar (⇑(Q i)) (x i) (y i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>P : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>CommRing R<VAR>(i : ι) → AddCommGroup (Mᵢ i)<VAR>AddCommGroup P<VAR>(i : ι) → Module R (Mᵢ i)<VAR>Module R P<VAR>Fintype ι<VAR>Q : (i : ι) → QuadraticMap R (Mᵢ i) P<GOAL>(QuadraticMap.pi Q).polarBilin = ∑ i : ι, LinearMap.compl₁₂ (Q i).polarBilin (LinearMap.proj i) (LinearMap.proj i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>P : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>CommRing R<VAR>(i : ι) → AddCommGroup (Mᵢ i)<VAR>AddCommGroup P<VAR>(i : ι) → Module R (Mᵢ i)<VAR>Module R P<VAR>Fintype ι<VAR>Invertible 2<VAR>Q : (i : ι) → QuadraticMap R (Mᵢ i) P<GOAL>QuadraticMap.associated (QuadraticMap.pi Q) = ∑ i : ι, LinearMap.compl₁₂ (QuadraticMap.associated (Q i)) (LinearMap.proj i) (LinearMap.proj i)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>V : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>AddCommGroup V<VAR>Algebra R A<VAR>Module R V<VAR>Invertible 2<VAR>Q : QuadraticForm R V<VAR>v : V<GOAL>(CliffordAlgebra.ofBaseChangeAux A Q) ((CliffordAlgebra.ι Q) v) = (CliffordAlgebra.ι (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] v)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>V : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>AddCommGroup V<VAR>Algebra R A<VAR>Module R V<VAR>Invertible 2<VAR>Q : QuadraticForm R V<VAR>z : A<VAR>v : V<GOAL>(CliffordAlgebra.ofBaseChange A Q) (z ⊗ₜ[R] (CliffordAlgebra.ι Q) v) = (CliffordAlgebra.ι (QuadraticForm.baseChange A Q)) (z ⊗ₜ[R] v)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>V : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>AddCommGroup V<VAR>Algebra R A<VAR>Module R V<VAR>Invertible 2<VAR>Q : QuadraticForm R V<VAR>z : A<GOAL>(CliffordAlgebra.ofBaseChange A Q) (z ⊗ₜ[R] 1) = (algebraMap A (CliffordAlgebra (QuadraticForm.baseChange A Q))) z
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>V : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>AddCommGroup V<VAR>Algebra R A<VAR>Module R V<VAR>Invertible 2<VAR>Q : QuadraticForm R V<VAR>z : A<VAR>v : V<GOAL>(CliffordAlgebra.toBaseChange A Q) ((CliffordAlgebra.ι (QuadraticForm.baseChange A Q)) (z ⊗ₜ[R] v)) = z ⊗ₜ[R] (CliffordAlgebra.ι Q) v
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>V : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>AddCommGroup V<VAR>Algebra R A<VAR>Module R V<VAR>Invertible 2<VAR>Q : QuadraticForm R V<GOAL>(CliffordAlgebra.toBaseChange A Q).comp CliffordAlgebra.involute = (Algebra.TensorProduct.map (AlgHom.id A A) CliffordAlgebra.involute).comp (CliffordAlgebra.toBaseChange A Q)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>V : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>AddCommGroup V<VAR>Algebra R A<VAR>Module R V<VAR>Invertible 2<VAR>Q : QuadraticForm R V<VAR>x : CliffordAlgebra (QuadraticForm.baseChange A Q)<GOAL>(CliffordAlgebra.toBaseChange A Q) (CliffordAlgebra.involute x) = (TensorProduct.map LinearMap.id CliffordAlgebra.involute.toLinearMap) ((CliffordAlgebra.toBaseChange A Q) x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>V : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>AddCommGroup V<VAR>Algebra R A<VAR>Module R V<VAR>Invertible 2<VAR>Q : QuadraticForm R V<GOAL>(AlgHom.op (CliffordAlgebra.toBaseChange A Q)).comp CliffordAlgebra.reverseOp = (↑(Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q))).comp ((Algebra.TensorProduct.map (↑(AlgEquiv.toOpposite A A)) CliffordAlgebra.reverseOp).comp (CliffordAlgebra.toBaseChange A Q))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>V : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>AddCommGroup V<VAR>Algebra R A<VAR>Module R V<VAR>Invertible 2<VAR>Q : QuadraticForm R V<VAR>x : CliffordAlgebra (QuadraticForm.baseChange A Q)<GOAL>(CliffordAlgebra.toBaseChange A Q) (CliffordAlgebra.reverse x) = (TensorProduct.map LinearMap.id CliffordAlgebra.reverse) ((CliffordAlgebra.toBaseChange A Q) x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>V : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>AddCommGroup V<VAR>Algebra R A<VAR>Module R V<VAR>Invertible 2<VAR>Q : QuadraticForm R V<GOAL>(CliffordAlgebra.toBaseChange A Q).comp (CliffordAlgebra.ofBaseChange A Q) = AlgHom.id A (A ⊗[R] CliffordAlgebra Q)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>V : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>AddCommGroup V<VAR>Algebra R A<VAR>Module R V<VAR>Invertible 2<VAR>Q : QuadraticForm R V<VAR>x : A ⊗[R] CliffordAlgebra Q<GOAL>(CliffordAlgebra.toBaseChange A Q) ((CliffordAlgebra.ofBaseChange A Q) x) = x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>V : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>AddCommGroup V<VAR>Algebra R A<VAR>Module R V<VAR>Invertible 2<VAR>Q : QuadraticForm R V<GOAL>(CliffordAlgebra.ofBaseChange A Q).comp (CliffordAlgebra.toBaseChange A Q) = AlgHom.id A (CliffordAlgebra (QuadraticForm.baseChange A Q))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>V : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>AddCommGroup V<VAR>Algebra R A<VAR>Module R V<VAR>Invertible 2<VAR>Q : QuadraticForm R V<VAR>x : CliffordAlgebra (QuadraticForm.baseChange A Q)<GOAL>(CliffordAlgebra.ofBaseChange A Q) ((CliffordAlgebra.toBaseChange A Q) x) = x