ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>DivisionSemiring R<VAR>StarRing R<VAR>x : R<VAR>hx : IsSelfAdjoint x<VAR>n : ℤ<GOAL>IsSelfAdjoint (x ^ n)
<VAR>R : Type u_1<VAR>DivisionSemiring R<VAR>StarRing R<VAR>q : ℚ≥0<GOAL>IsSelfAdjoint ↑q
<VAR>R : Type u_1<VAR>DivisionRing R<VAR>StarRing R<VAR>x : ℚ<GOAL>IsSelfAdjoint ↑x
<VAR>R : Type u_1<VAR>Semifield R<VAR>StarRing R<VAR>x y : R<VAR>hx : IsSelfAdjoint x<VAR>hy : IsSelfAdjoint y<GOAL>IsSelfAdjoint (x / y)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Star R<VAR>AddMonoid A<VAR>StarAddMonoid A<VAR>SMul R A<VAR>StarModule R A<VAR>r : R<VAR>hr : IsSelfAdjoint r<VAR>x : A<VAR>hx : IsSelfAdjoint x<GOAL>IsSelfAdjoint (r • x)
<VAR>R : Type u_1<VAR>AddGroup R<VAR>StarAddMonoid R<VAR>x : R<GOAL>x ∈ selfAdjoint R ↔ star x = x
<VAR>R : Type u_1<VAR>AddGroup R<VAR>StarAddMonoid R<VAR>x : ↥(selfAdjoint R)<GOAL>star ↑x = ↑x
<VAR>R : Type u_1<VAR>Ring R<VAR>StarRing R<GOAL>↑1 = 1
<VAR>R : Type u_1<VAR>Ring R<VAR>StarRing R<VAR>x : ↥(selfAdjoint R)<VAR>n : ℕ<GOAL>↑(x ^ n) = ↑x ^ n
<VAR>R : Type u_1<VAR>NonUnitalCommRing R<VAR>StarRing R<VAR>x y : ↥(selfAdjoint R)<GOAL>↑(x * y) = ↑x * ↑y
<VAR>R : Type u_1<VAR>Field R<VAR>StarRing R<VAR>x : ↥(selfAdjoint R)<GOAL>↑x⁻¹ = (↑x)⁻¹
<VAR>R : Type u_1<VAR>Field R<VAR>StarRing R<VAR>x y : ↥(selfAdjoint R)<GOAL>↑(x / y) = ↑x / ↑y
<VAR>R : Type u_1<VAR>Field R<VAR>StarRing R<VAR>x : ↥(selfAdjoint R)<VAR>z : ℤ<GOAL>↑(x ^ z) = ↑x ^ z
<VAR>R : Type u_1<VAR>Field R<VAR>StarRing R<VAR>q : ℚ≥0<GOAL>↑↑q = ↑q
<VAR>R : Type u_1<VAR>Field R<VAR>StarRing R<VAR>q : ℚ<GOAL>↑↑q = ↑q
<VAR>R : Type u_1<VAR>Field R<VAR>StarRing R<VAR>q : ℚ≥0<VAR>x : ↥(selfAdjoint R)<GOAL>↑(q • x) = q • ↑x
<VAR>R : Type u_1<VAR>Field R<VAR>StarRing R<VAR>q : ℚ<VAR>x : ↥(selfAdjoint R)<GOAL>↑(q • x) = q • ↑x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Star R<VAR>TrivialStar R<VAR>AddGroup A<VAR>StarAddMonoid A<VAR>SMul R A<VAR>StarModule R A<VAR>r : R<VAR>x : ↥(selfAdjoint A)<GOAL>↑(r • x) = r • ↑x
<VAR>R : Type u_1<VAR>AddCommGroup R<VAR>StarAddMonoid R<VAR>x : R<GOAL>x ∈ skewAdjoint R ↔ star x = -x
<VAR>R : Type u_1<VAR>AddCommGroup R<VAR>StarAddMonoid R<VAR>x : ↥(skewAdjoint R)<GOAL>star ↑x = -↑x
<VAR>R : Type u_1<VAR>Ring R<VAR>StarRing R<VAR>x : R<VAR>hx : x ∈ skewAdjoint R<VAR>z : R<GOAL>z * x * star z ∈ skewAdjoint R
<VAR>R : Type u_1<VAR>Ring R<VAR>StarRing R<VAR>x : R<VAR>hx : x ∈ skewAdjoint R<VAR>z : R<GOAL>star z * x * z ∈ skewAdjoint R
<VAR>R : Type u_1<VAR>Ring R<VAR>StarRing R<VAR>x : R<VAR>hx : x ∈ skewAdjoint R<GOAL>IsStarNormal x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Star R<VAR>TrivialStar R<VAR>AddCommGroup A<VAR>StarAddMonoid A<VAR>Monoid R<VAR>DistribMulAction R A<VAR>StarModule R A<VAR>r : R<VAR>x : A<VAR>h : x ∈ skewAdjoint A<GOAL>r • x ∈ skewAdjoint A
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Star R<VAR>TrivialStar R<VAR>AddCommGroup A<VAR>StarAddMonoid A<VAR>Monoid R<VAR>DistribMulAction R A<VAR>StarModule R A<VAR>r : R<VAR>x : ↥(skewAdjoint A)<GOAL>↑(r • x) = r • ↑x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Ring R<VAR>AddCommGroup A<VAR>Module R A<VAR>StarAddMonoid R<VAR>StarAddMonoid A<VAR>StarModule R A<VAR>r : R<VAR>hr : r ∈ skewAdjoint R<VAR>a : A<VAR>ha : IsSelfAdjoint a<GOAL>r • a ∈ skewAdjoint A
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Ring R<VAR>AddCommGroup A<VAR>Module R A<VAR>StarAddMonoid R<VAR>StarAddMonoid A<VAR>StarModule R A<VAR>r : R<VAR>hr : r ∈ skewAdjoint R<VAR>a : A<VAR>ha : a ∈ skewAdjoint A<GOAL>IsSelfAdjoint (r • a)
<VAR>ι : Type u_3<VAR>α : ι → Type u_4<VAR>(i : ι) → Star (α i)<VAR>f : (i : ι) → α i<GOAL>IsSelfAdjoint f ↔ ∀ (i : ι), IsSelfAdjoint (f i)
<VAR>R : Type u<VAR>Ring R<VAR>M : FGModuleCat R<GOAL>↑M.obj = ↑M
<VAR>R : Type u<VAR>Ring R<VAR>V W : Type u<VAR>AddCommGroup V<VAR>Module R V<VAR>Module.Finite R V<VAR>AddCommGroup W<VAR>Module R W<VAR>Module.Finite R W<VAR>e : V ≃ₗ[R] W<GOAL>e.toFGModuleCatIso.inv = ↑e.symm
<VAR>R : Type u<VAR>Ring R<VAR>V W : Type u<VAR>AddCommGroup V<VAR>Module R V<VAR>Module.Finite R V<VAR>AddCommGroup W<VAR>Module R W<VAR>Module.Finite R W<VAR>e : V ≃ₗ[R] W<GOAL>e.toFGModuleCatIso.hom = ↑e
<VAR>R : Type u<VAR>CommRing R<GOAL>(𝟙_ (FGModuleCat R)).obj = 𝟙_ (ModuleCat R)
<VAR>R : Type u<VAR>CommRing R<VAR>M N : FGModuleCat R<GOAL>(CategoryTheory.MonoidalCategory.tensorObj M N).obj = CategoryTheory.MonoidalCategory.tensorObj M.obj N.obj
<VAR>R : Type u<VAR>CommRing R<VAR>V W : FGModuleCat R<VAR>i : V ≅ W<VAR>f : CategoryTheory.End V<GOAL>i.conj f = (FGModuleCat.isoToLinearEquiv i).conj f
<VAR>K : Type u<VAR>Field K<VAR>V W : FGModuleCat K<GOAL>(CategoryTheory.ihom V).obj W = FGModuleCat.of K (↑V →ₗ[K] ↑W)
<VAR>K : Type u<VAR>Field K<VAR>V : FGModuleCat K<GOAL>(FGModuleCat.FGModuleCatDual K V).obj = ModuleCat.of K (Module.Dual K ↑V)
<VAR>K : Type u<VAR>Field K<VAR>V : FGModuleCat K<GOAL>↑(FGModuleCat.FGModuleCatDual K V) = Module.Dual K ↑V
<VAR>K : Type u<VAR>Field K<VAR>V : FGModuleCat K<GOAL>(FGModuleCat.FGModuleCatCoevaluation K V) 1 = ∑ i : ↑(Basis.ofVectorSpaceIndex K ↑V), (Basis.ofVectorSpace K ↑V) i ⊗ₜ[K] (Basis.ofVectorSpace K ↑V).coord i
<VAR>K : Type u<VAR>Field K<VAR>V : FGModuleCat K<VAR>f : ↑(FGModuleCat.FGModuleCatDual K V)<VAR>x : ↑V<GOAL>(FGModuleCat.FGModuleCatEvaluation K V) (f ⊗ₜ[K] x) = f.toFun x
<VAR>K : Type u<VAR>Field K<VAR>V : FGModuleCat K<GOAL>CategoryTheory.MonoidalCategory.whiskerLeft (FGModuleCat.FGModuleCatDual K V) (FGModuleCat.FGModuleCatCoevaluation K V) ≫ (CategoryTheory.MonoidalCategory.associator (FGModuleCat.FGModuleCatDual K V) V (FGModuleCat.FGModuleCatDual K V)).inv ≫ CategoryTheory.MonoidalCategory.whiskerRight (FGModuleCat.FGModuleCatEvaluation K V) (FGModuleCat.FGModuleCatDual K V) = (CategoryTheory.MonoidalCategory.rightUnitor (FGModuleCat.FGModuleCatDual K V)).hom ≫ (CategoryTheory.MonoidalCategory.leftUnitor (FGModuleCat.FGModuleCatDual K V)).inv
<VAR>K : Type u<VAR>Field K<VAR>V : FGModuleCat K<GOAL>CategoryTheory.MonoidalCategory.whiskerRight (FGModuleCat.FGModuleCatCoevaluation K V) V ≫ (CategoryTheory.MonoidalCategory.associator V (FGModuleCat.FGModuleCatDual K V) V).hom ≫ CategoryTheory.MonoidalCategory.whiskerLeft V (FGModuleCat.FGModuleCatEvaluation K V) = (CategoryTheory.MonoidalCategory.leftUnitor V).hom ≫ (CategoryTheory.MonoidalCategory.rightUnitor V).inv
<VAR>R : Type u<VAR>Ring R<VAR>G : FGModuleCat R<VAR>H : Type u<VAR>AddCommGroup H<VAR>Module R H<VAR>f : ↑G →ₗ[R] H<GOAL>f ∘ₗ 𝟙 G = f
<VAR>R : Type u<VAR>Ring R<VAR>G : Type u<VAR>AddCommGroup G<VAR>Module R G<VAR>H : FGModuleCat R<VAR>f : G →ₗ[R] ↑H<GOAL>𝟙 H ∘ₗ f = f
<VAR>α : Type u_1<VAR>BooleanRing α<GOAL>↑(BoolRing.of α) = α
<VAR>α β : BoolRing<VAR>e : ↑α ≃+* ↑β<GOAL>(BoolRing.Iso.mk e).hom = ↑e
<VAR>α β : BoolRing<VAR>e : ↑α ≃+* ↑β<GOAL>(BoolRing.Iso.mk e).inv = ↑e.symm
<VAR>X Y : BoolRing<VAR>f : ↑X →+* ↑Y<GOAL>CategoryTheory.HasForget₂.forget₂.map f = f.asBoolAlg
<VAR>X : BoolRing<GOAL>CategoryTheory.HasForget₂.forget₂.obj X = BoolAlg.of (AsBoolAlg ↑X)
<VAR>X : BoolAlg<GOAL>CategoryTheory.HasForget₂.forget₂.obj X = BoolRing.of (AsBoolRing ↑X)
<VAR>X Y : BoolAlg<VAR>f : BoundedLatticeHom ↑X.toBddDistLat.toBddLat.toLat ↑Y.toBddDistLat.toBddLat.toLat<GOAL>CategoryTheory.HasForget₂.forget₂.map f = f.asBoolRing
<GOAL>boolRingCatEquivBoolAlg.inverse = CategoryTheory.forget₂ BoolAlg BoolRing
<GOAL>boolRingCatEquivBoolAlg.functor = CategoryTheory.forget₂ BoolRing BoolAlg
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>NormedLinearOrderedField K<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>b : Basis ι K E<GOAL>Submodule.span K ↑(Submodule.span ℤ (Set.range ⇑b)) = ⊤
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>NormedLinearOrderedField K<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>b : Basis ι K E<VAR>m : E<GOAL>m ∈ Zspan.fundamentalDomain b ↔ ∀ (i : ι), (b.repr m) i ∈ Set.Ico 0 1
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>NormedLinearOrderedField K<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>b : Basis ι K E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace K F<VAR>f : E ≃ₗ[K] F<GOAL>⇑f '' Zspan.fundamentalDomain b = Zspan.fundamentalDomain (b.map f)
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>NormedLinearOrderedField K<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>b : Basis ι K E<VAR>ι' : Type u_4<VAR>e : ι ≃ ι'<GOAL>Zspan.fundamentalDomain (b.reindex e) = Zspan.fundamentalDomain b
<VAR>ι : Type u_2<VAR>Fintype ι<GOAL>Zspan.fundamentalDomain (Pi.basisFun ℝ ι) = Set.univ.pi fun x => Set.Ico 0 1
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>NormedLinearOrderedField K<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>b : Basis ι K E<VAR>FloorRing K<VAR>Fintype ι<VAR>m : E<VAR>i : ι<GOAL>(b.repr ↑(Zspan.floor b m)) i = ↑⌊(b.repr m) i⌋
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>NormedLinearOrderedField K<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>b : Basis ι K E<VAR>FloorRing K<VAR>Fintype ι<VAR>m : E<VAR>i : ι<GOAL>(b.repr ↑(Zspan.ceil b m)) i = ↑⌈(b.repr m) i⌉
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>NormedLinearOrderedField K<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>b : Basis ι K E<VAR>FloorRing K<VAR>Fintype ι<VAR>m : E<VAR>h : m ∈ Submodule.span ℤ (Set.range ⇑b)<GOAL>↑(Zspan.floor b m) = m
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>NormedLinearOrderedField K<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>b : Basis ι K E<VAR>FloorRing K<VAR>Fintype ι<VAR>m : E<VAR>h : m ∈ Submodule.span ℤ (Set.range ⇑b)<GOAL>↑(Zspan.ceil b m) = m
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>NormedLinearOrderedField K<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>b : Basis ι K E<VAR>FloorRing K<VAR>Fintype ι<VAR>m : E<GOAL>Zspan.fract b m = m - ↑(Zspan.floor b m)
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>NormedLinearOrderedField K<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>b : Basis ι K E<VAR>FloorRing K<VAR>Fintype ι<VAR>m : E<VAR>i : ι<GOAL>(b.repr (Zspan.fract b m)) i = Int.fract ((b.repr m) i)
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>NormedLinearOrderedField K<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>b : Basis ι K E<VAR>FloorRing K<VAR>Fintype ι<VAR>m : E<GOAL>Zspan.fract b (Zspan.fract b m) = Zspan.fract b m
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>NormedLinearOrderedField K<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>b : Basis ι K E<VAR>FloorRing K<VAR>Fintype ι<VAR>m : E<VAR>v : E<VAR>h : v ∈ Submodule.span ℤ (Set.range ⇑b)<GOAL>Zspan.fract b (v + m) = Zspan.fract b m
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>NormedLinearOrderedField K<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>b : Basis ι K E<VAR>FloorRing K<VAR>Fintype ι<VAR>m : E<VAR>v : E<VAR>h : v ∈ Submodule.span ℤ (Set.range ⇑b)<GOAL>Zspan.fract b (m + v) = Zspan.fract b m
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>NormedLinearOrderedField K<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>b : Basis ι K E<VAR>FloorRing K<VAR>Fintype ι<VAR>x : E<GOAL>Zspan.fract b x = x ↔ x ∈ Zspan.fundamentalDomain b
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>NormedLinearOrderedField K<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>b : Basis ι K E<VAR>FloorRing K<VAR>Fintype ι<VAR>x : E<GOAL>Zspan.fract b x ∈ Zspan.fundamentalDomain b
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>NormedLinearOrderedField K<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>b : Basis ι K E<VAR>FloorRing K<VAR>Fintype ι<GOAL>Function.Surjective (Zspan.fractRestrict b)
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>NormedLinearOrderedField K<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>b : Basis ι K E<VAR>FloorRing K<VAR>Fintype ι<VAR>x : E<GOAL>↑(Zspan.fractRestrict b x) = Zspan.fract b x
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>NormedLinearOrderedField K<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>b : Basis ι K E<VAR>FloorRing K<VAR>Fintype ι<VAR>m n : E<GOAL>Zspan.fract b m = Zspan.fract b n ↔ -m + n ∈ Submodule.span ℤ (Set.range ⇑b)
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>NormedLinearOrderedField K<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>b : Basis ι K E<VAR>FloorRing K<VAR>Fintype ι<VAR>HasSolidNorm K<VAR>m : E<GOAL>‖Zspan.fract b m‖ ≤ ∑ i : ι, ‖b i‖
<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>NormedLinearOrderedField K<VAR>FloorRing K<VAR>Fintype ι<VAR>Unique ι<VAR>k : K<GOAL>↑(Zspan.floor (Basis.singleton ι K) k) = ↑⌊k⌋
<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>NormedLinearOrderedField K<VAR>FloorRing K<VAR>Fintype ι<VAR>Unique ι<VAR>k : K<GOAL>Zspan.fract (Basis.singleton ι K) k = Int.fract k
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>NormedLinearOrderedField K<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>b : Basis ι K E<VAR>FloorRing K<VAR>Finite ι<VAR>HasSolidNorm K<GOAL>Bornology.IsBounded (Zspan.fundamentalDomain b)
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>NormedLinearOrderedField K<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>b : Basis ι K E<VAR>FloorRing K<VAR>Fintype ι<VAR>y : ↥(Submodule.span ℤ (Set.range ⇑b))<VAR>x : E<GOAL>y +ᵥ x ∈ Zspan.fundamentalDomain b ↔ y = -Zspan.floor b x
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>NormedLinearOrderedField K<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>b : Basis ι K E<VAR>FloorRing K<VAR>Finite ι<VAR>x : E<GOAL>∃! v, v +ᵥ x ∈ Zspan.fundamentalDomain b
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>NormedLinearOrderedField K<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>b : Basis ι K E<VAR>FloorRing K<VAR>Fintype ι<VAR>x : E<GOAL>(Zspan.quotientEquiv b) (Submodule.Quotient.mk x) = Zspan.fractRestrict b x
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>NormedLinearOrderedField K<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>b : Basis ι K E<VAR>FloorRing K<VAR>Fintype ι<VAR>x : ↑(Zspan.fundamentalDomain b)<GOAL>(Zspan.quotientEquiv b).symm x = Submodule.Quotient.mk ↑x
<VAR>ι : Type u_2<VAR>Finite ι<GOAL>DiscreteTopology ↥(Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>b : Basis ι ℝ E<VAR>Fintype ι<GOAL>Zspan.fundamentalDomain b ⊆ parallelepiped ⇑b
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>b : Basis ι ℝ E<VAR>MeasurableSpace E<VAR>OpensMeasurableSpace E<VAR>Finite ι<GOAL>MeasurableSet (Zspan.fundamentalDomain b)
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>b : Basis ι ℝ E<VAR>Finite ι<VAR>MeasurableSpace E<VAR>OpensMeasurableSpace E<VAR>μ : MeasureTheory.Measure E<GOAL>MeasureTheory.IsAddFundamentalDomain (↥(Submodule.span ℤ (Set.range ⇑b)).toAddSubgroup) (Zspan.fundamentalDomain b) μ
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>b : Basis ι ℝ E<VAR>Finite ι<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<GOAL>μ (Zspan.fundamentalDomain b) ≠ 0
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>b : Basis ι ℝ E<VAR>Fintype ι<VAR>DecidableEq ι<VAR>MeasurableSpace E<VAR>μ : MeasureTheory.Measure E<VAR>BorelSpace E<VAR>μ.IsAddHaarMeasure<VAR>b₀ : Basis ι ℝ E<GOAL>μ (Zspan.fundamentalDomain b) = ENNReal.ofReal |b₀.det ⇑b| * μ (Zspan.fundamentalDomain b₀)
<VAR>ι : Type u_2<VAR>Fintype ι<VAR>DecidableEq ι<VAR>b : Basis ι ℝ (ι → ℝ)<GOAL>MeasureTheory.volume (Zspan.fundamentalDomain b) = ENNReal.ofReal |(Matrix.of ⇑b).det|
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>b : Basis ι ℝ E<VAR>Fintype ι<VAR>MeasurableSpace E<VAR>μ : MeasureTheory.Measure E<VAR>BorelSpace E<VAR>μ.IsAddHaarMeasure<GOAL>Zspan.fundamentalDomain b =ᵐ[μ] parallelepiped ⇑b
<VAR>K : Type u_1<VAR>NormedField K<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>L : AddSubgroup E<VAR>DiscreteTopology ↥L<VAR>self : IsZlattice K L<GOAL>Submodule.span K ↑L = ⊤
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>Finite ι<VAR>b : Basis ι ℝ E<GOAL>IsZlattice ℝ (Submodule.span ℤ (Set.range ⇑b)).toAddSubgroup
<VAR>K : Type u_1<VAR>NormedLinearOrderedField K<VAR>HasSolidNorm K<VAR>FloorRing K<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>FiniteDimensional K E<VAR>ProperSpace E<VAR>L : AddSubgroup E<VAR>DiscreteTopology ↥L<VAR>hs : IsZlattice K L<GOAL>L.FG
<VAR>K : Type u_1<VAR>NormedLinearOrderedField K<VAR>HasSolidNorm K<VAR>FloorRing K<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>FiniteDimensional K E<VAR>ProperSpace E<VAR>L : AddSubgroup E<VAR>DiscreteTopology ↥L<VAR>IsZlattice K L<GOAL>Module.Finite ℤ ↥L
<VAR>K : Type u_1<VAR>NormedLinearOrderedField K<VAR>HasSolidNorm K<VAR>FloorRing K<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>FiniteDimensional K E<VAR>ProperSpace E<VAR>L : AddSubgroup E<VAR>DiscreteTopology ↥L<VAR>IsZlattice K L<GOAL>Module.Free ℤ ↥L
<VAR>K : Type u_1<VAR>NormedLinearOrderedField K<VAR>HasSolidNorm K<VAR>FloorRing K<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>FiniteDimensional K E<VAR>ProperSpace E<VAR>L : AddSubgroup E<VAR>DiscreteTopology ↥L<VAR>hs : IsZlattice K L<GOAL>FiniteDimensional.finrank ℤ ↥L = FiniteDimensional.finrank K E
<VAR>K : Type u_1<VAR>NormedLinearOrderedField K<VAR>HasSolidNorm K<VAR>FloorRing K<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>FiniteDimensional K E<VAR>ProperSpace E<VAR>L : AddSubgroup E<VAR>DiscreteTopology ↥L<VAR>ι : Type u_3<VAR>hs : IsZlattice K L<VAR>b : Basis ι ℤ ↥L<VAR>i : ι<GOAL>(Basis.ofZlatticeBasis K L b) i = ↑(b i)
<VAR>K : Type u_1<VAR>NormedLinearOrderedField K<VAR>HasSolidNorm K<VAR>FloorRing K<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>FiniteDimensional K E<VAR>ProperSpace E<VAR>L : AddSubgroup E<VAR>DiscreteTopology ↥L<VAR>ι : Type u_3<VAR>hs : IsZlattice K L<VAR>b : Basis ι ℤ ↥L<VAR>x : ↥L<VAR>i : ι<GOAL>((Basis.ofZlatticeBasis K L b).repr ↑x) i = ↑((b.repr x) i)
<VAR>K : Type u_1<VAR>NormedLinearOrderedField K<VAR>HasSolidNorm K<VAR>FloorRing K<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>FiniteDimensional K E<VAR>ProperSpace E<VAR>L : AddSubgroup E<VAR>DiscreteTopology ↥L<VAR>ι : Type u_3<VAR>hs : IsZlattice K L<VAR>b : Basis ι ℤ ↥L<GOAL>(Submodule.span ℤ (Set.range ⇑(Basis.ofZlatticeBasis K L b))).toAddSubgroup = L
<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>L : AddSubgroup E<VAR>DiscreteTopology ↥L<VAR>IsZlattice ℝ L<VAR>Finite ι<VAR>b : Basis ι ℤ ↥L<VAR>MeasurableSpace E<VAR>OpensMeasurableSpace E<VAR>μ : MeasureTheory.Measure E<GOAL>MeasureTheory.IsAddFundamentalDomain (↥L) (Zspan.fundamentalDomain (Basis.ofZlatticeBasis ℝ L b)) μ
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsKilling R L<VAR>IsNoetherian R L<VAR>IsArtinian R L<VAR>H : LieSubalgebra R L<VAR>H.IsCartanSubalgebra<GOAL>LinearMap.ker ((killingForm R L).restrict H.toSubmodule) = ⊥
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>H : LieSubalgebra R L<GOAL>(killingForm R L).restrict H.toSubmodule = LieModule.traceForm R (↥H) L
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsKilling R L<VAR>IsNoetherian R L<VAR>IsArtinian R L<VAR>H : LieSubalgebra R L<VAR>H.IsCartanSubalgebra<GOAL>LinearMap.ker (LieModule.traceForm R (↥H) L) = ⊥
<VAR>R : Type u_1<VAR>L : Type u_3<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieAlgebra.IsKilling R L<VAR>IsNoetherian R L<VAR>IsArtinian R L<VAR>H : LieSubalgebra R L<VAR>H.IsCartanSubalgebra<GOAL>(LieModule.traceForm R (↥H) L).Nondegenerate
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α β : ↥H → K<VAR>x y : L<VAR>hx : x ∈ LieAlgebra.rootSpace H α<VAR>hy : y ∈ LieAlgebra.rootSpace H β<VAR>hαβ : α + β ≠ 0<GOAL>((killingForm K L) x) y = 0
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>α : ↥H → K<VAR>x : L<VAR>hx : x ∈ LieAlgebra.rootSpace H α<VAR>hx' : ∀ y ∈ LieAlgebra.rootSpace H (-α), ((killingForm K L) x) y = 0<GOAL>x ∈ LinearMap.ker (killingForm K L)
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieAlgebra.IsKilling K L<VAR>x : L<VAR>hx : x ∈ H<VAR>hx' : IsNilpotent ((LieAlgebra.ad K L) x)<GOAL>x = 0
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieAlgebra.IsKilling K L<GOAL>∀ (a m : ↥H), ((LieAlgebra.IsKilling.cartanEquivDual H) a) m = (LinearMap.trace K L) ((LieModule.toEnd K (↥H) L) a * (LieModule.toEnd K (↥H) L) m)
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>LieAlgebra.IsKilling K L<VAR>α : LieModule.Weight K (↥H) L<VAR>e f : L<VAR>heα : e ∈ LieAlgebra.rootSpace H ⇑α<VAR>hfα : f ∈ LieAlgebra.rootSpace H (-⇑α)<VAR>aux : ∀ (h : ↥H), ⁅h, e⁆ = α h • e<GOAL>⁅e, f⁆ = ((killingForm K L) e) f • ↑((LieAlgebra.IsKilling.cartanEquivDual H).symm (LieModule.Weight.toLinear K (↥H) L α))
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>LieAlgebra.IsKilling K L<VAR>α : LieModule.Weight K (↥H) L<GOAL>(LieAlgebra.IsKilling.cartanEquivDual H).symm (LieModule.Weight.toLinear K (↥H) L α) ∈ LieAlgebra.corootSpace ⇑α
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>LieAlgebra.IsKilling K L<GOAL>Submodule.span K (Set.range (LieModule.Weight.toLinear K (↥H) L)) = ⊤
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>LieAlgebra.IsKilling K L<GOAL>Submodule.span K (LieModule.Weight.toLinear K (↥H) L '' {α | α.IsNonZero}) = ⊤
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>LieAlgebra.IsKilling K L<GOAL>⨅ α, LieModule.Weight.ker = ⊥
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieAlgebra.IsKilling K L<GOAL>LieAlgebra.corootSpace 0 = ⊥
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>LieAlgebra.IsKilling K L<VAR>PerfectField K<VAR>x : L<VAR>hx : x ∈ H<GOAL>((LieAlgebra.ad K L) x).IsSemisimple
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>LieAlgebra.IsKilling K L<VAR>PerfectField K<VAR>α : ↥H → K<VAR>x : L<VAR>hx : x ∈ LieAlgebra.rootSpace H α<VAR>h : ↥H<GOAL>⁅h, x⁆ = α h • x
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>LieRing L<VAR>Field K<VAR>LieAlgebra K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<VAR>LieAlgebra.IsKilling K L<VAR>PerfectField K<VAR>α : LieModule.Weight K (↥H) L<VAR>e f : L<VAR>heα : e ∈ LieAlgebra.rootSpace H ⇑α<VAR>hfα : f ∈ LieAlgebra.rootSpace H (-⇑α)<GOAL>⁅e, f⁆ = ((killingForm K L) e) f • ↑((LieAlgebra.IsKilling.cartanEquivDual H).symm (LieModule.Weight.toLinear K (↥H) L α))