ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>q : QuaternionAlgebra R c₁ c₂<GOAL>CliffordAlgebraQuaternion.ofQuaternion (star q) = star (CliffordAlgebraQuaternion.ofQuaternion q)
<VAR>R : Type u_1<VAR>CommRing R<VAR>r₁ r₂ : R<GOAL>(CliffordAlgebra.ι 0) r₁ * (CliffordAlgebra.ι 0) r₂ = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>r : R<GOAL>CliffordAlgebraDualNumber.equiv ((CliffordAlgebra.ι 0) r) = r • DualNumber.eps
<VAR>R : Type u_1<VAR>CommRing R<GOAL>CliffordAlgebraDualNumber.equiv.symm DualNumber.eps = (CliffordAlgebra.ι 0) 1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<GOAL>1 ≤ CliffordAlgebra.evenOdd Q 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<GOAL>LinearMap.range (CliffordAlgebra.ι Q) ≤ CliffordAlgebra.evenOdd Q 1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>m : M<GOAL>(CliffordAlgebra.ι Q) m ∈ CliffordAlgebra.evenOdd Q 1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>m₁ m₂ : M<GOAL>(CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ ∈ CliffordAlgebra.evenOdd Q 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>i j : ZMod 2<GOAL>CliffordAlgebra.evenOdd Q i * CliffordAlgebra.evenOdd Q j ≤ CliffordAlgebra.evenOdd Q (i + j)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>m : M<GOAL>(CliffordAlgebra.GradedAlgebra.ι Q) m = (DirectSum.of (fun i => ↥(CliffordAlgebra.evenOdd Q i)) 1) ⟨(CliffordAlgebra.ι Q) m, ⋯⟩
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>m : M<GOAL>(CliffordAlgebra.GradedAlgebra.ι Q) m * (CliffordAlgebra.GradedAlgebra.ι Q) m = (algebraMap R (DirectSum (ZMod 2) fun i => ↥(CliffordAlgebra.evenOdd Q i))) (Q m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>i' : ZMod 2<VAR>x' : ↥(CliffordAlgebra.evenOdd Q i')<GOAL>((CliffordAlgebra.lift Q) ⟨CliffordAlgebra.GradedAlgebra.ι Q, ⋯⟩) ↑x' = (DirectSum.of (fun i => ↥(CliffordAlgebra.evenOdd Q i)) i') x'
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<GOAL>⨆ i, LinearMap.range (CliffordAlgebra.ι Q) ^ i = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<GOAL>IsCompl (CliffordAlgebra.evenOdd Q 0) (CliffordAlgebra.evenOdd Q 1)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>n : ZMod 2<VAR>motive : (x : CliffordAlgebra Q) → x ∈ CliffordAlgebra.evenOdd Q n → Prop<VAR>range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (CliffordAlgebra.ι Q) ^ n.val), motive v ⋯<VAR>add : ∀ (x y : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd Q n) (hy : y ∈ CliffordAlgebra.evenOdd Q n), motive x hx → motive y hy → motive (x + y) ⋯<VAR>ι_mul_ι_mul : ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd Q n), motive x hx → motive ((CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x) ⋯<VAR>x : CliffordAlgebra Q<VAR>hx : x ∈ CliffordAlgebra.evenOdd Q n<GOAL>motive x hx
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>motive : (x : CliffordAlgebra Q) → x ∈ CliffordAlgebra.evenOdd Q 0 → Prop<VAR>algebraMap : ∀ (r : R), motive ((algebraMap R (CliffordAlgebra Q)) r) ⋯<VAR>add : ∀ (x y : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd Q 0) (hy : y ∈ CliffordAlgebra.evenOdd Q 0), motive x hx → motive y hy → motive (x + y) ⋯<VAR>ι_mul_ι_mul : ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd Q 0), motive x hx → motive ((CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x) ⋯<VAR>x : CliffordAlgebra Q<VAR>hx : x ∈ CliffordAlgebra.evenOdd Q 0<GOAL>motive x hx
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>P : (x : CliffordAlgebra Q) → x ∈ CliffordAlgebra.evenOdd Q 1 → Prop<VAR>ι : ∀ (v : M), P ((CliffordAlgebra.ι Q) v) ⋯<VAR>add : ∀ (x y : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd Q 1) (hy : y ∈ CliffordAlgebra.evenOdd Q 1), P x hx → P y hy → P (x + y) ⋯<VAR>ι_mul_ι_mul : ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd Q 1), P x hx → P ((CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x) ⋯<VAR>x : CliffordAlgebra Q<VAR>hx : x ∈ CliffordAlgebra.evenOdd Q 1<GOAL>P x hx
<VAR>R : Type u_2<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>N : Type u_9<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid N<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R N<VAR>Q₁ : QuadraticMap R M₁ N<VAR>Q₂ : QuadraticMap R M₂ N<VAR>self : Q₁.IsometryEquiv Q₂<VAR>m : M₁<GOAL>Q₂ ((↑self.toLinearEquiv).toFun m) = Q₁ m
<VAR>R : Type u_2<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>N : Type u_9<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid N<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R N<VAR>Q₁ : QuadraticMap R M₁ N<VAR>Q₂ : QuadraticMap R M₂ N<VAR>f : Q₁.IsometryEquiv Q₂<GOAL>⇑f.toLinearEquiv = ⇑f
<VAR>R : Type u_2<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>N : Type u_9<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid N<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R N<VAR>Q₁ : QuadraticMap R M₁ N<VAR>Q₂ : QuadraticMap R M₂ N<VAR>f : Q₁.IsometryEquiv Q₂<VAR>m : M₁<GOAL>Q₂ (f m) = Q₁ m
<VAR>R : Type u_2<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>N : Type u_9<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid N<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R N<VAR>Q₁ : QuadraticMap R M₁ N<VAR>Q₂ : QuadraticMap R M₂ N<VAR>g : Q₁.IsometryEquiv Q₂<VAR>x : M₁<GOAL>g.toIsometry x = g x
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>N : Type u_9<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.Equivalent Q
<VAR>R : Type u_2<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>N : Type u_9<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid N<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R N<VAR>Q₁ : QuadraticMap R M₁ N<VAR>Q₂ : QuadraticMap R M₂ N<VAR>h : Q₁.Equivalent Q₂<GOAL>Q₂.Equivalent Q₁
<VAR>R : Type u_2<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>N : Type u_9<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>AddCommMonoid N<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R M₃<VAR>Module R N<VAR>Q₁ : QuadraticMap R M₁ N<VAR>Q₂ : QuadraticMap R M₂ N<VAR>Q₃ : QuadraticMap R M₃ N<VAR>h : Q₁.Equivalent Q₂<VAR>h' : Q₂.Equivalent Q₃<GOAL>Q₁.Equivalent Q₃
<VAR>K : Type u_3<VAR>V : Type u_8<VAR>Field K<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>Q : QuadraticForm K V<GOAL>∃ w, QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares K w)
<VAR>K : Type u_3<VAR>V : Type u_8<VAR>Field K<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>Q : QuadraticForm K V<VAR>hQ : LinearMap.SeparatingLeft (QuadraticMap.associated Q)<GOAL>∃ w, QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares K w)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>m : M<GOAL>(CliffordAlgebra.ι Q) m * (CliffordAlgebra.ι Q) m = (algebraMap R (CliffordAlgebra Q)) (Q m)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>A : Type u_3<VAR>Semiring A<VAR>Algebra R A<VAR>g : CliffordAlgebra Q →ₐ[R] A<VAR>m : M<GOAL>g ((CliffordAlgebra.ι Q) m) * g ((CliffordAlgebra.ι Q) m) = (algebraMap R A) (Q m)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>A : Type u_3<VAR>Semiring A<VAR>Algebra R A<VAR>F : CliffordAlgebra Q →ₐ[R] A<GOAL>(CliffordAlgebra.lift Q).symm F = ⟨F.toLinearMap ∘ₗ CliffordAlgebra.ι Q, ⋯⟩
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>A : Type u_3<VAR>Semiring A<VAR>Algebra R A<VAR>f : M →ₗ[R] A<VAR>cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)<GOAL>((CliffordAlgebra.lift Q) ⟨f, cond⟩).toLinearMap ∘ₗ CliffordAlgebra.ι Q = f
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>A : Type u_3<VAR>Semiring A<VAR>Algebra R A<VAR>f : M →ₗ[R] A<VAR>cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)<VAR>x : M<GOAL>((CliffordAlgebra.lift Q) ⟨f, cond⟩) ((CliffordAlgebra.ι Q) x) = f x
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>A : Type u_3<VAR>Semiring A<VAR>Algebra R A<VAR>f : M →ₗ[R] A<VAR>cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)<VAR>g : CliffordAlgebra Q →ₐ[R] A<GOAL>g.toLinearMap ∘ₗ CliffordAlgebra.ι Q = f ↔ g = (CliffordAlgebra.lift Q) ⟨f, cond⟩
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>A : Type u_3<VAR>Semiring A<VAR>Algebra R A<VAR>g : CliffordAlgebra Q →ₐ[R] A<GOAL>(CliffordAlgebra.lift Q) ⟨g.toLinearMap ∘ₗ CliffordAlgebra.ι Q, ⋯⟩ = g
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>A : Type u_4<VAR>Semiring A<VAR>Algebra R A<VAR>f g : CliffordAlgebra Q →ₐ[R] A<GOAL>f.toLinearMap ∘ₗ CliffordAlgebra.ι Q = g.toLinearMap ∘ₗ CliffordAlgebra.ι Q → f = g
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>C : CliffordAlgebra Q → Prop<VAR>algebraMap : ∀ (r : R), C ((algebraMap R (CliffordAlgebra Q)) r)<VAR>ι : ∀ (x : M), C ((CliffordAlgebra.ι Q) x)<VAR>mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)<VAR>add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)<VAR>a : CliffordAlgebra Q<GOAL>C a
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>A : Type u_4<VAR>Ring A<VAR>Algebra R A<VAR>f : M →ₗ[R] A<VAR>hf : ∀ (x : M), f x * f x = (algebraMap R A) (Q x)<VAR>a b : M<GOAL>f a * f b + f b * f a = (algebraMap R A) (QuadraticMap.polar (⇑Q) a b)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>A : Type u_4<VAR>Ring A<VAR>Algebra R A<VAR>h2 : IsUnit 2<VAR>f : M →ₗ[R] A<GOAL>(∀ (x : M), f x * f x = (algebraMap R A) (Q x)) ↔ (LinearMap.mul R A).compl₂ f ∘ₗ f + (LinearMap.mul R A).flip.compl₂ f ∘ₗ f = LinearMap.compr₂ (QuadraticMap.polarBilin Q) (Algebra.linearMap R A)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>a b : M<GOAL>(CliffordAlgebra.ι Q) a * (CliffordAlgebra.ι Q) b + (CliffordAlgebra.ι Q) b * (CliffordAlgebra.ι Q) a = (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>a b : M<GOAL>(CliffordAlgebra.ι Q) a * (CliffordAlgebra.ι Q) b = (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) - (CliffordAlgebra.ι Q) b * (CliffordAlgebra.ι Q) a
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>a b : M<VAR>h : QuadraticMap.IsOrtho Q a b<GOAL>(CliffordAlgebra.ι Q) a * (CliffordAlgebra.ι Q) b + (CliffordAlgebra.ι Q) b * (CliffordAlgebra.ι Q) a = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>a b : M<VAR>h : QuadraticMap.IsOrtho Q a b<GOAL>(CliffordAlgebra.ι Q) a * (CliffordAlgebra.ι Q) b = -((CliffordAlgebra.ι Q) b * (CliffordAlgebra.ι Q) a)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>x : CliffordAlgebra Q<VAR>a b : M<VAR>h : QuadraticMap.IsOrtho Q a b<GOAL>x * (CliffordAlgebra.ι Q) a * (CliffordAlgebra.ι Q) b = -(x * (CliffordAlgebra.ι Q) b * (CliffordAlgebra.ι Q) a)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>x : CliffordAlgebra Q<VAR>a b : M<VAR>h : QuadraticMap.IsOrtho Q a b<GOAL>(CliffordAlgebra.ι Q) a * ((CliffordAlgebra.ι Q) b * x) = -((CliffordAlgebra.ι Q) b * ((CliffordAlgebra.ι Q) a * x))
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>a b : M<GOAL>(CliffordAlgebra.ι Q) a * (CliffordAlgebra.ι Q) b * (CliffordAlgebra.ι Q) a = (CliffordAlgebra.ι Q) (QuadraticMap.polar (⇑Q) a b • a - Q a • b)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>A : Type u_3<VAR>Semiring A<VAR>Algebra R A<VAR>f : M →ₗ[R] A<VAR>cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)<GOAL>Submodule.map ((CliffordAlgebra.lift Q) ⟨f, cond⟩).toLinearMap (LinearMap.range (CliffordAlgebra.ι Q)) = LinearMap.range f
<VAR>R : Type u_1<VAR>CommRing R<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>f : Q₁ →qᵢ Q₂<GOAL>(CliffordAlgebra.map f).toLinearMap ∘ₗ CliffordAlgebra.ι Q₁ = CliffordAlgebra.ι Q₂ ∘ₗ f.toLinearMap
<VAR>R : Type u_1<VAR>CommRing R<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>f : Q₁ →qᵢ Q₂<VAR>m : M₁<GOAL>(CliffordAlgebra.map f) ((CliffordAlgebra.ι Q₁) m) = (CliffordAlgebra.ι Q₂) (f m)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M₁ : Type u_4<VAR>AddCommGroup M₁<VAR>Module R M₁<VAR>Q₁ : QuadraticForm R M₁<GOAL>CliffordAlgebra.map (QuadraticMap.Isometry.id Q₁) = AlgHom.id R (CliffordAlgebra Q₁)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>AddCommGroup M₃<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R M₃<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>f : Q₂ →qᵢ Q₃<VAR>g : Q₁ →qᵢ Q₂<GOAL>(CliffordAlgebra.map f).comp (CliffordAlgebra.map g) = CliffordAlgebra.map (f.comp g)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>f : Q₁ →qᵢ Q₂<GOAL>Submodule.map (CliffordAlgebra.map f).toLinearMap (LinearMap.range (CliffordAlgebra.ι Q₁)) = Submodule.map (CliffordAlgebra.ι Q₂) (LinearMap.range f.toLinearMap)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>f : Q₁ →qᵢ Q₂<VAR>g : Q₂ →qᵢ Q₁<VAR>h : Function.LeftInverse ⇑g ⇑f<GOAL>Function.LeftInverse ⇑(CliffordAlgebra.map g) ⇑(CliffordAlgebra.map f)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>f : Q₁ →qᵢ Q₂<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Surjective ⇑(CliffordAlgebra.map f)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>e : QuadraticMap.IsometryEquiv Q₁ Q₂<VAR>a : CliffordAlgebra Q₁<GOAL>(CliffordAlgebra.equivOfIsometry e) a = (CliffordAlgebra.map e.toIsometry) a
<VAR>R : Type u_1<VAR>CommRing R<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>e : QuadraticMap.IsometryEquiv Q₁ Q₂<GOAL>(CliffordAlgebra.equivOfIsometry e).symm = CliffordAlgebra.equivOfIsometry e.symm
<VAR>R : Type u_1<VAR>CommRing R<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>AddCommGroup M₃<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R M₃<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>e₁₂ : QuadraticMap.IsometryEquiv Q₁ Q₂<VAR>e₂₃ : QuadraticMap.IsometryEquiv Q₂ Q₃<GOAL>(CliffordAlgebra.equivOfIsometry e₁₂).trans (CliffordAlgebra.equivOfIsometry e₂₃) = CliffordAlgebra.equivOfIsometry (e₁₂.trans e₂₃)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M₁ : Type u_4<VAR>AddCommGroup M₁<VAR>Module R M₁<VAR>Q₁ : QuadraticForm R M₁<GOAL>CliffordAlgebra.equivOfIsometry (QuadraticMap.IsometryEquiv.refl Q₁) = AlgEquiv.refl
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>m : M<GOAL>TensorAlgebra.toClifford ((TensorAlgebra.ι R) m) = (CliffordAlgebra.ι Q) m
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module ℝ M<VAR>FiniteDimensional ℝ M<VAR>Q : QuadraticForm ℝ M<VAR>hQ : LinearMap.SeparatingLeft (QuadraticMap.associated Q)<GOAL>∃ w, (∀ (i : Fin (FiniteDimensional.finrank ℝ M)), w i ≠ 0) ∧ QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares ℝ fun i => ↑(w i))
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module ℝ M<VAR>FiniteDimensional ℝ M<VAR>Q : QuadraticForm ℝ M<VAR>hQ : LinearMap.SeparatingLeft (QuadraticMap.associated Q)<GOAL>∃ w, (∀ (i : Fin (FiniteDimensional.finrank ℝ M)), w i = -1 ∨ w i = 1) ∧ QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares ℝ w)
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module ℝ M<VAR>FiniteDimensional ℝ M<VAR>Q : QuadraticForm ℝ M<GOAL>∃ w, QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares ℝ fun i => ↑(w i))
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module ℝ M<VAR>FiniteDimensional ℝ M<VAR>Q : QuadraticForm ℝ M<GOAL>∃ w, (∀ (i : Fin (FiniteDimensional.finrank ℝ M)), w i = -1 ∨ w i = 0 ∨ w i = 1) ∧ QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares ℝ w)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>a : Module.Dual R M × M<GOAL>∀ (a_1 : Module.Dual R M × M), ((LinearMap.dualProd R M) a) a_1 = a_1.1 a.2 + a.1 a_1.2
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>LinearMap.IsSymm (LinearMap.dualProd R M)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<GOAL>LinearMap.SeparatingLeft (LinearMap.dualProd R M) ↔ Function.Injective ⇑(Module.Dual.eval R M)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Module.Dual R M × M<GOAL>(QuadraticForm.dualProd R M) p = p.1 p.2
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>LinearMap.BilinMap.toQuadraticMap (LinearMap.dualProd R M) = 2 • QuadraticForm.dualProd R M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>f : M ≃ₗ[R] N<GOAL>∀ (a : Module.Dual R M × M), (QuadraticForm.dualProdIsometry f) a = ((↑f.symm.dualMap).prodCongr ↑f) a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>f : M ≃ₗ[R] N<GOAL>∀ (a : Module.Dual R N × N), (QuadraticForm.dualProdIsometry f).invFun a = ((↑f.symm.dualMap).prodCongr ↑f).symm a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<GOAL>∀ (a : (Module.Dual R M × M) × Module.Dual R N × N), QuadraticForm.dualProdProdIsometry.invFun a = ((Module.dualProdDualEquivDual R M N).symm.prod (LinearEquiv.refl R (M × N))).symm ((a.1.1, a.2.1), a.1.2, a.2.2)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<GOAL>∀ (a : Module.Dual R (M × N) × M × N), QuadraticForm.dualProdProdIsometry a = ((a.1 ∘ₗ LinearMap.inl R M N, a.2.1), a.1 ∘ₗ LinearMap.inr R M N, a.2.2)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>Invertible 2<VAR>i : M × M<GOAL>Q.toDualProd i = ((QuadraticMap.associated Q) i.1 + (QuadraticMap.associated Q) i.2, i.1 - i.2)
<VAR>R : Type u<VAR>CommRing R<VAR>X : QuadraticModuleCat R<GOAL>ModuleCat.of R ↑X.toModuleCat = X.toModuleCat
<VAR>R : Type u<VAR>CommRing R<VAR>X : Type v<VAR>AddCommGroup X<VAR>Module R X<VAR>Q : QuadraticForm R X<GOAL>(QuadraticModuleCat.of Q).form = Q
<VAR>R : Type u<VAR>CommRing R<VAR>V W : QuadraticModuleCat R<GOAL>Function.Injective QuadraticModuleCat.Hom.toIsometry
<VAR>R : Type u<VAR>CommRing R<VAR>M N : QuadraticModuleCat R<VAR>f g : M ⟶ N<VAR>h : f.toIsometry = g.toIsometry<GOAL>f = g
<VAR>R : Type u<VAR>CommRing R<VAR>M N U : QuadraticModuleCat R<VAR>f : M ⟶ N<VAR>g : N ⟶ U<GOAL>(f ≫ g).toIsometry = g.toIsometry.comp f.toIsometry
<VAR>R : Type u<VAR>CommRing R<VAR>M : QuadraticModuleCat R<GOAL>(𝟙 M).toIsometry = QuadraticMap.Isometry.id M.form
<VAR>R : Type u<VAR>CommRing R<VAR>X : QuadraticModuleCat R<GOAL>(CategoryTheory.forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj X = ModuleCat.of R ↑X.toModuleCat
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : QuadraticModuleCat R<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.forget₂ (QuadraticModuleCat R) (ModuleCat R)).map f = f.toIsometry.toLinearMap
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : Type v<VAR>AddCommGroup X<VAR>Module R X<VAR>AddCommGroup Y<VAR>Module R Y<VAR>Q₁ : QuadraticForm R X<VAR>Q₂ : QuadraticForm R Y<VAR>e : QuadraticMap.IsometryEquiv Q₁ Q₂<GOAL>(QuadraticModuleCat.ofIso e).hom.toIsometry = e.toIsometry
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : Type v<VAR>AddCommGroup X<VAR>Module R X<VAR>AddCommGroup Y<VAR>Module R Y<VAR>Q₁ : QuadraticForm R X<VAR>Q₂ : QuadraticForm R Y<VAR>e : QuadraticMap.IsometryEquiv Q₁ Q₂<GOAL>(QuadraticModuleCat.ofIso e).inv.toIsometry = e.symm.toIsometry
<VAR>R : Type u<VAR>CommRing R<VAR>X : Type v<VAR>AddCommGroup X<VAR>Module R X<VAR>Q₁ : QuadraticForm R X<GOAL>QuadraticModuleCat.ofIso (QuadraticMap.IsometryEquiv.refl Q₁) = CategoryTheory.Iso.refl (QuadraticModuleCat.of Q₁)
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : Type v<VAR>AddCommGroup X<VAR>Module R X<VAR>AddCommGroup Y<VAR>Module R Y<VAR>Q₁ : QuadraticForm R X<VAR>Q₂ : QuadraticForm R Y<VAR>e : QuadraticMap.IsometryEquiv Q₁ Q₂<GOAL>QuadraticModuleCat.ofIso e.symm = (QuadraticModuleCat.ofIso e).symm
<VAR>R : Type u<VAR>CommRing R<VAR>X Y Z : Type v<VAR>AddCommGroup X<VAR>Module R X<VAR>AddCommGroup Y<VAR>Module R Y<VAR>AddCommGroup Z<VAR>Module R Z<VAR>Q₁ : QuadraticForm R X<VAR>Q₂ : QuadraticForm R Y<VAR>Q₃ : QuadraticForm R Z<VAR>e : QuadraticMap.IsometryEquiv Q₁ Q₂<VAR>f : QuadraticMap.IsometryEquiv Q₂ Q₃<GOAL>QuadraticModuleCat.ofIso (e.trans f) = QuadraticModuleCat.ofIso e ≪≫ QuadraticModuleCat.ofIso f
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : QuadraticModuleCat R<VAR>i : X ≅ Y<VAR>a : ↑Y.toModuleCat<GOAL>i.toIsometryEquiv.invFun a = i.inv.toIsometry a
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : QuadraticModuleCat R<VAR>i : X ≅ Y<VAR>a : ↑X.toModuleCat<GOAL>i.toIsometryEquiv a = i.hom.toIsometry a
<VAR>R : Type u<VAR>CommRing R<VAR>X : QuadraticModuleCat R<GOAL>(CategoryTheory.Iso.refl X).toIsometryEquiv = QuadraticMap.IsometryEquiv.refl X.form
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : QuadraticModuleCat R<VAR>e : X ≅ Y<GOAL>e.symm.toIsometryEquiv = e.toIsometryEquiv.symm
<VAR>R : Type u<VAR>CommRing R<VAR>X Y Z : QuadraticModuleCat R<VAR>e : X ≅ Y<VAR>f : Y ≅ Z<GOAL>(e ≪≫ f).toIsometryEquiv = e.toIsometryEquiv.trans f.toIsometryEquiv