ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>r₁ r₂ : R<VAR>s₁ s₂ : ↥S<GOAL>r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r₁ * r₂ /ₒ (s₁ * s₂)
<VAR>R : Type u_1<VAR>AddCommMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>r₁ r₂ : R<VAR>s₁ s₂ : ↥S<GOAL>r₁ -ₒ s₁ + (r₂ -ₒ s₂) = r₁ + r₂ -ₒ (s₁ + s₂)
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>Zero X<VAR>MulAction R X<GOAL>0 = 0 /ₒ 1
<VAR>R : Type u_1<VAR>MonoidWithZero R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>s : ↥S<GOAL>0 /ₒ s = 0
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>AddMonoid X<VAR>DistribMulAction R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : X<VAR>s₂ : ↥S<VAR>rb sb : R<VAR>hb : sb * ↑s₁ = rb * ↑s₂<VAR>h : sb * ↑s₁ ∈ S<GOAL>OreLocalization.add'' r₁ s₁ r₂ s₂ = (sb • r₁ + rb • r₂) /ₒ ⟨sb * ↑s₁, h⟩
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>AddMonoid X<VAR>DistribMulAction R X<VAR>r r' : X<VAR>s s' : ↥S<GOAL>r /ₒ s + r' /ₒ s' = (OreLocalization.oreDenom (↑s) s' • r + OreLocalization.oreNum (↑s) s' • r') /ₒ (OreLocalization.oreDenom (↑s) s' * s)
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>AddMonoid X<VAR>DistribMulAction R X<VAR>r r' : X<VAR>s s' : ↥S<VAR>rb sb : R<VAR>h : sb * ↑s = rb * ↑s'<VAR>h' : sb * ↑s ∈ S<GOAL>r /ₒ s + r' /ₒ s' = (sb • r + rb • r') /ₒ ⟨sb * ↑s, h'⟩
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>AddMonoid X<VAR>DistribMulAction R X<VAR>r r' : X<VAR>s s' : ↥S<VAR>rb : R<VAR>sb : ↥S<VAR>h : ↑sb * ↑s = rb * ↑s'<GOAL>r /ₒ s + r' /ₒ s' = (sb • r + rb • r') /ₒ (sb * s)
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>AddMonoid X<VAR>DistribMulAction R X<VAR>r r' : X<VAR>s : ↥S<GOAL>r /ₒ s + r' /ₒ s = (r + r') /ₒ s
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>AddMonoid X<VAR>DistribMulAction R X<VAR>x y z : OreLocalization S X<GOAL>x + y + z = x + (y + z)
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>AddMonoid X<VAR>DistribMulAction R X<VAR>s : ↥S<GOAL>0 /ₒ s = 0
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>AddMonoid X<VAR>DistribMulAction R X<VAR>x : OreLocalization S X<GOAL>0 + x = x
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>AddMonoid X<VAR>DistribMulAction R X<VAR>x : OreLocalization S X<GOAL>x + 0 = x
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>AddMonoid X<VAR>DistribMulAction R X<VAR>x : OreLocalization S R<GOAL>x • 0 = 0
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>AddMonoid X<VAR>DistribMulAction R X<VAR>z : OreLocalization S R<VAR>x y : OreLocalization S X<GOAL>z • (x + y) = z • x + z • y
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>AddCommMonoid X<VAR>DistribMulAction R X<VAR>x y : OreLocalization S X<GOAL>x + y = y + x
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>AddGroup X<VAR>DistribMulAction R X<VAR>r : X<VAR>s : ↥S<GOAL>-(r /ₒ s) = -r /ₒ s
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>AddGroup X<VAR>DistribMulAction R X<VAR>x : OreLocalization S X<GOAL>-x + x = 0
<VAR>R : Type u_2<VAR>S : Type u_3<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>IsDomain S<VAR>F : Type u_4<VAR>CommRing F<VAR>Algebra F R<VAR>Algebra F S<VAR>IsScalarTower F R S<VAR>I : Ideal S<VAR>hI : I ≠ ⊥<VAR>ι : Type u_5<VAR>Fintype ι<VAR>b : Basis ι R S<VAR>Nontrivial F<VAR>∀ (i : ι), Module.Free F (R ⧸ Ideal.span {Ideal.smithCoeffs b I hI i})<VAR>∀ (i : ι), Module.Finite F (R ⧸ Ideal.span {Ideal.smithCoeffs b I hI i})<GOAL>FiniteDimensional.finrank F (S ⧸ I) = ∑ i : ι, FiniteDimensional.finrank F (R ⧸ Ideal.span {Ideal.smithCoeffs b I hI i})
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommMonoid N<VAR>Module R N<VAR>ι : Type u_4<VAR>e : M ≃ₗ[R] N<VAR>v : M [⋀^ι]→ₗ[R] R<VAR>hv : v ≠ 0<GOAL>(Orientation.map ι e) (rayOfNeZero R v hv) = rayOfNeZero R (v.compLinearMap ↑e.symm) ⋯
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_4<GOAL>Orientation.map ι (LinearEquiv.refl R M) = Equiv.refl (Orientation R M ι)
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommMonoid N<VAR>Module R N<VAR>ι : Type u_4<VAR>e : M ≃ₗ[R] N<GOAL>(Orientation.map ι e).symm = Orientation.map ι e.symm
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>e : ι ≃ ι'<VAR>v : M [⋀^ι]→ₗ[R] R<VAR>hv : v ≠ 0<GOAL>(Orientation.reindex R M e) (rayOfNeZero R v hv) = rayOfNeZero R (AlternatingMap.domDomCongr e v) ⋯
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_4<GOAL>Orientation.reindex R M (Equiv.refl ι) = Equiv.refl (Orientation R M ι)
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>e : ι ≃ ι'<GOAL>(Orientation.reindex R M e).symm = Orientation.reindex R M e.symm
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommMonoid N<VAR>Module R N<VAR>ι : Type u_4<VAR>IsEmpty ι<VAR>f : M ≃ₗ[R] N<GOAL>(Orientation.map ι f) positiveOrientation = positiveOrientation
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_4<VAR>IsEmpty ι<VAR>x : Orientation R M ι<VAR>f : M ≃ₗ[R] M<GOAL>(Orientation.map ι f) x = x
<VAR>R : Type u_1<VAR>StrictOrderedCommRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>ι : Type u_4<VAR>f : M ≃ₗ[R] N<VAR>x : Orientation R M ι<GOAL>(Orientation.map ι f) (-x) = -(Orientation.map ι f) x
<VAR>R : Type u_1<VAR>StrictOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>e : ι ≃ ι'<VAR>x : Orientation R M ι<GOAL>(Orientation.reindex R M e) (-x) = -(Orientation.reindex R M e) x
<VAR>R : Type u_1<VAR>StrictOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_4<VAR>Finite ι<VAR>e : Basis ι R M<VAR>x : Orientation R M ι<VAR>f : M ≃ₗ[R] M<GOAL>(Orientation.map ι f) x = (LinearEquiv.det f)⁻¹ • x
<VAR>R : Type u_1<VAR>StrictOrderedCommRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>ι : Type u_4<VAR>Fintype ι<VAR>DecidableEq ι<VAR>e : Basis ι R M<VAR>f : M ≃ₗ[R] N<GOAL>(e.map f).orientation = (Orientation.map ι f) e.orientation
<VAR>R : Type u_1<VAR>StrictOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>Fintype ι<VAR>DecidableEq ι<VAR>Fintype ι'<VAR>DecidableEq ι'<VAR>e : Basis ι R M<VAR>eι : ι ≃ ι'<GOAL>(e.reindex eι).orientation = (Orientation.reindex R M eι) e.orientation
<VAR>R : Type u_1<VAR>StrictOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_4<VAR>Fintype ι<VAR>DecidableEq ι<VAR>e : Basis ι R M<VAR>w : ι → Rˣ<GOAL>(e.unitsSMul w).orientation = (∏ i : ι, w i)⁻¹ • e.orientation
<VAR>R : Type u_1<VAR>StrictOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_4<VAR>Fintype ι<VAR>DecidableEq ι<VAR>IsEmpty ι<VAR>b : Basis ι R M<GOAL>b.orientation = positiveOrientation
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_3<VAR>IsEmpty ι<VAR>o : Orientation R M ι<GOAL>o = positiveOrientation ∨ o = -positiveOrientation
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_3<VAR>Fintype ι<VAR>DecidableEq ι<VAR>e₁ e₂ : Basis ι R M<GOAL>e₁.orientation = e₂.orientation ↔ 0 < e₁.det ⇑e₂
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_3<VAR>Fintype ι<VAR>DecidableEq ι<VAR>e : Basis ι R M<VAR>x : Orientation R M ι<GOAL>x = e.orientation ∨ x = -e.orientation
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_3<VAR>Fintype ι<VAR>DecidableEq ι<VAR>e : Basis ι R M<VAR>x : Orientation R M ι<GOAL>x ≠ e.orientation ↔ x = -e.orientation
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_3<VAR>Fintype ι<VAR>DecidableEq ι<VAR>e : Basis ι R M<VAR>f : M ≃ₗ[R] M<GOAL>(e.map f).orientation = e.orientation ↔ 0 < LinearMap.det ↑f
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_3<VAR>Fintype ι<VAR>DecidableEq ι<VAR>e : Basis ι R M<VAR>f : M ≃ₗ[R] M<GOAL>(e.map f).orientation = -e.orientation ↔ LinearMap.det ↑f < 0
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_3<VAR>Fintype ι<VAR>DecidableEq ι<VAR>e : Basis ι R M<VAR>i : ι<GOAL>(e.unitsSMul (Function.update 1 i (-1))).orientation = -e.orientation
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_3<VAR>Fintype ι<VAR>DecidableEq ι<VAR>Nonempty ι<VAR>e : Basis ι R M<VAR>x : Orientation R M ι<GOAL>(e.adjustToOrientation x).orientation = x
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_3<VAR>Fintype ι<VAR>DecidableEq ι<VAR>Nonempty ι<VAR>e : Basis ι R M<VAR>x : Orientation R M ι<VAR>i : ι<GOAL>(e.adjustToOrientation x) i = e i ∨ (e.adjustToOrientation x) i = -e i
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_3<VAR>Fintype ι<VAR>DecidableEq ι<VAR>Nonempty ι<VAR>e : Basis ι R M<VAR>x : Orientation R M ι<GOAL>(e.adjustToOrientation x).det = e.det ∨ (e.adjustToOrientation x).det = -e.det
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_3<VAR>Fintype ι<VAR>DecidableEq ι<VAR>Nonempty ι<VAR>e : Basis ι R M<VAR>x : Orientation R M ι<VAR>v : ι → M<GOAL>|(e.adjustToOrientation x).det v| = |e.det v|
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_3<VAR>Fintype ι<VAR>_i : FiniteDimensional R M<VAR>x₁ x₂ : Orientation R M ι<VAR>h : Fintype.card ι = FiniteDimensional.finrank R M<GOAL>x₁ = x₂ ∨ x₁ = -x₂
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_3<VAR>Fintype ι<VAR>_i : FiniteDimensional R M<VAR>x₁ x₂ : Orientation R M ι<VAR>h : Fintype.card ι = FiniteDimensional.finrank R M<GOAL>x₁ ≠ x₂ ↔ x₁ = -x₂
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_3<VAR>Fintype ι<VAR>_i : FiniteDimensional R M<VAR>x : Orientation R M ι<VAR>f : M ≃ₗ[R] M<VAR>h : Fintype.card ι = FiniteDimensional.finrank R M<GOAL>(Orientation.map ι f) x = (LinearEquiv.det f)⁻¹ • x
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_3<VAR>Fintype ι<VAR>_i : FiniteDimensional R M<VAR>x : Orientation R M ι<VAR>f : M ≃ₗ[R] M<VAR>h : Fintype.card ι = FiniteDimensional.finrank R M<GOAL>(Orientation.map ι f) x = x ↔ 0 < LinearMap.det ↑f
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_3<VAR>Fintype ι<VAR>x : Orientation R M ι<VAR>f : M ≃ₗ[R] M<VAR>h : Fintype.card ι = FiniteDimensional.finrank R M<GOAL>(Orientation.map ι f) x = -x ↔ LinearMap.det ↑f < 0
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_3<VAR>Fintype ι<VAR>_i : FiniteDimensional R M<VAR>Nonempty ι<VAR>DecidableEq ι<VAR>x : Orientation R M ι<VAR>h : Fintype.card ι = FiniteDimensional.finrank R M<GOAL>(x.someBasis h).orientation = x
<VAR>R : Type u<VAR>CommRing R<VAR>M : QuadraticModuleCat R<GOAL>↑(QuadraticModuleCat.cliffordAlgebra.obj M) = CliffordAlgebra M.form
<VAR>R : Type u<VAR>CommRing R<VAR>_M _N : QuadraticModuleCat R<VAR>f : _M ⟶ _N<GOAL>QuadraticModuleCat.cliffordAlgebra.map f = CliffordAlgebra.map f.toIsometry
<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<GOAL>star x = CliffordAlgebra.reverse (CliffordAlgebra.involute 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>x : CliffordAlgebra Q<GOAL>star x = CliffordAlgebra.involute (CliffordAlgebra.reverse 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>m : M<GOAL>star ((CliffordAlgebra.ι Q) m) = -(CliffordAlgebra.ι 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>r : R<VAR>x : CliffordAlgebra Q<GOAL>star (r • x) = r • star 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>r : R<GOAL>star ((algebraMap R (CliffordAlgebra Q)) r) = (algebraMap R (CliffordAlgebra Q)) r
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : LinearMap.GeneralLinearGroup R M<GOAL>↑((LinearMap.GeneralLinearGroup.generalLinearEquiv R M) f) = ↑f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : LinearMap.GeneralLinearGroup R M<GOAL>⇑((LinearMap.GeneralLinearGroup.generalLinearEquiv R M) f) = ⇑↑f
<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<VAR>Invertible (Q m)<VAR>Invertible ((CliffordAlgebra.ι Q) m)<GOAL>⅟((CliffordAlgebra.ι Q) m) = (CliffordAlgebra.ι Q) (⅟(Q m) • 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<VAR>h : IsUnit (Q m)<GOAL>IsUnit ((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>a b : M<VAR>Invertible ((CliffordAlgebra.ι Q) a)<VAR>Invertible (Q a)<GOAL>(CliffordAlgebra.ι Q) a * (CliffordAlgebra.ι Q) b * ⅟((CliffordAlgebra.ι Q) a) = (CliffordAlgebra.ι Q) ((⅟(Q a) * QuadraticMap.polar (⇑Q) a b) • a - b)
<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>a b : M<VAR>Invertible ((CliffordAlgebra.ι Q) a)<VAR>Invertible (Q a)<GOAL>⅟((CliffordAlgebra.ι Q) a) * (CliffordAlgebra.ι Q) b * (CliffordAlgebra.ι Q) a = (CliffordAlgebra.ι Q) ((⅟(Q a) * QuadraticMap.polar (⇑Q) a b) • a - b)
<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>m : M<VAR>h : IsUnit ((CliffordAlgebra.ι Q) m)<GOAL>IsUnit (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>Invertible 2<VAR>m : M<GOAL>IsUnit ((CliffordAlgebra.ι Q) m) ↔ IsUnit (Q m)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>p : PerfectPairing R M N<VAR>root : ι ↪ M<VAR>coroot : ι ↪ N<VAR>i j : ι<VAR>h : ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (root i) (p.toLin.flip (coroot i)))) (Set.range ⇑root) (Set.range ⇑root)<GOAL>∃ k, root k = (Module.preReflection (root i) (p.toLin.flip (coroot i))) (root j)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>p : PerfectPairing R M N<VAR>root : ι ↪ M<VAR>coroot : ι ↪ N<VAR>i j : ι<VAR>h : ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (root i) (p.toLin.flip (coroot i)))) (Set.range ⇑root) (Set.range ⇑root)<VAR>hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2<GOAL>⋯.choose = j
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>p : PerfectPairing R M N<VAR>root : ι ↪ M<VAR>coroot : ι ↪ N<VAR>i : ι<VAR>h : ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (root i) (p.toLin.flip (coroot i)))) (Set.range ⇑root) (Set.range ⇑root)<VAR>hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2<VAR>j : ι<GOAL>(RootPairing.equiv_of_mapsTo p root coroot i h hp) j = ⋯.choose
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>p : PerfectPairing R M N<VAR>root : ι ↪ M<VAR>coroot : ι ↪ N<VAR>i : ι<VAR>h : ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (root i) (p.toLin.flip (coroot i)))) (Set.range ⇑root) (Set.range ⇑root)<VAR>hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2<VAR>j : ι<GOAL>(RootPairing.equiv_of_mapsTo p root coroot i h hp).symm j = ⋯.choose
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>Finite ι<VAR>P : RootPairing ι R M N<VAR>NoZeroSMulDivisors ℤ M<GOAL>Set.InjOn (⇑((Submodule.span R (Set.range ⇑P.root)).subtype.dualMap ∘ₗ P.toLin.flip)) (Set.range ⇑P.coroot)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>Finite ι<VAR>CharZero R<VAR>NoZeroSMulDivisors R M<VAR>P₁ P₂ : RootPairing ι R M N<VAR>he : P₁.toLin = P₂.toLin<VAR>hr : P₁.root = P₂.root<VAR>hc : Set.range ⇑P₁.coroot = Set.range ⇑P₂.coroot<GOAL>P₁ = P₂
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>Finite ι<VAR>CharZero R<VAR>NoZeroSMulDivisors R M<VAR>p : PerfectPairing R M N<VAR>root : ι ↪ M<VAR>coroot : ι ↪ N<VAR>hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2<VAR>hr : ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (root i) (p.toLin.flip (coroot i)))) (Set.range ⇑root) (Set.range ⇑root)<VAR>hc : ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (coroot i) (p.toLin (root i)))) (Set.range ⇑coroot) (Set.range ⇑coroot)<VAR>i j k : ι<VAR>hk : root k = (Module.preReflection (root i) (p.toLin.flip (coroot i))) (root j)<GOAL>coroot k = (Module.preReflection (coroot i) (p.toLin (root i))) (coroot j)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>Finite ι<VAR>CharZero R<VAR>NoZeroSMulDivisors R M<VAR>P₁ P₂ : RootSystem ι R M N<VAR>he : P₁.toLin = P₂.toLin<VAR>hr : P₁.root = P₂.root<GOAL>P₁ = P₂
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>Finite ι<VAR>CharZero R<VAR>NoZeroSMulDivisors R M<VAR>p : PerfectPairing R M N<VAR>root : ι ↪ M<VAR>coroot : ι ↪ N<VAR>hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2<VAR>hs : ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (root i) (p.toLin.flip (coroot i)))) (Set.range ⇑root) (Set.range ⇑root)<VAR>hsp : Submodule.span R (Set.range ⇑root) = ⊤<VAR>i j k : ι<VAR>hk : root k = (Module.preReflection (root i) (p.toLin.flip (coroot i))) (root j)<GOAL>coroot k = (Module.preReflection (coroot i) (p.toLin (root i))) (coroot j)
<VAR>R : Type u_2<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>N : Type u_8<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₁ →qᵢ Q₂<VAR>m : M₁<GOAL>Q₂ (self.toFun m) = Q₁ m
<VAR>R : Type u_2<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>N : Type u_8<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<GOAL>Function.Injective QuadraticMap.Isometry.toLinearMap
<VAR>R : Type u_2<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>N : Type u_8<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 g : Q₁ →qᵢ Q₂<VAR>h : ∀ (x : M₁), f x = g x<GOAL>f = g
<VAR>R : Type u_2<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>N : Type u_8<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₁ →qᵢ Q₂<VAR>m : M₁<GOAL>Q₂ (f m) = Q₁ m
<VAR>R : Type u_2<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>N : Type u_8<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₁ →qᵢ Q₂<GOAL>⇑f.toLinearMap = ⇑f
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_8<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticMap R M N<VAR>a : M<GOAL>(QuadraticMap.Isometry.id Q) a = a
<VAR>R : Type u_2<VAR>M₁ : Type u_4<VAR>N : Type u_8<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid N<VAR>Module R M₁<VAR>Module R N<VAR>Q₁ Q₂ : QuadraticMap R M₁ N<VAR>h : Q₁ = Q₂<VAR>a : M₁<GOAL>(QuadraticMap.Isometry.ofEq h) a = a
<VAR>R : Type u_2<VAR>M₁ : Type u_4<VAR>N : Type u_8<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid N<VAR>Module R M₁<VAR>Module R N<VAR>Q : QuadraticMap R M₁ N<GOAL>QuadraticMap.Isometry.ofEq ⋯ = QuadraticMap.Isometry.id Q
<VAR>R : Type u_2<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<VAR>N : Type u_8<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>g : Q₂ →qᵢ Q₃<VAR>f : Q₁ →qᵢ Q₂<VAR>x : M₁<GOAL>(g.comp f) x = g (f x)
<VAR>R : Type u_2<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<VAR>N : Type u_8<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>g : Q₂ →qᵢ Q₃<VAR>f : Q₁ →qᵢ Q₂<GOAL>(g.comp f).toLinearMap = g.toLinearMap ∘ₗ f.toLinearMap
<VAR>R : Type u_2<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>N : Type u_8<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₁ →qᵢ Q₂<GOAL>(QuadraticMap.Isometry.id Q₂).comp f = f
<VAR>R : Type u_2<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>N : Type u_8<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₁ →qᵢ Q₂<GOAL>f.comp (QuadraticMap.Isometry.id Q₁) = f
<VAR>R : Type u_2<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<VAR>M₄ : Type u_7<VAR>N : Type u_8<VAR>CommSemiring R<VAR>AddCommMonoid M₁<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 M₄<VAR>Module R N<VAR>Q₁ : QuadraticMap R M₁ N<VAR>Q₂ : QuadraticMap R M₂ N<VAR>Q₃ : QuadraticMap R M₃ N<VAR>Q₄ : QuadraticMap R M₄ N<VAR>h : Q₃ →qᵢ Q₄<VAR>g : Q₂ →qᵢ Q₃<VAR>f : Q₁ →qᵢ Q₂<GOAL>(h.comp g).comp f = h.comp (g.comp f)