ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>s : Set α<VAR>Countable G<VAR>MeasurableSpace G<VAR>MeasurableSpace α<VAR>MeasurableSMul G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>hs : MeasureTheory.NullMeasurableSet s μ<GOAL>MeasureTheory.NullMeasurableSet (MeasureTheory.fundamentalFrontier G s) μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>s : Set α<VAR>Countable G<VAR>MeasurableSpace G<VAR>MeasurableSpace α<VAR>MeasurableSMul G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>hs : MeasureTheory.NullMeasurableSet s μ<GOAL>MeasureTheory.NullMeasurableSet (MeasureTheory.fundamentalInterior G s) μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>s : Set α<VAR>Countable G<VAR>MeasurableSpace G<VAR>MeasurableSpace α<VAR>MeasurableVAdd G α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>hs : MeasureTheory.NullMeasurableSet s μ<GOAL>MeasureTheory.NullMeasurableSet (MeasureTheory.addFundamentalInterior G s) μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Countable G<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasureTheory.IsAddFundamentalDomain G s μ<GOAL>μ (MeasureTheory.addFundamentalFrontier G s) = 0
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Countable G<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasureTheory.IsFundamentalDomain G s μ<GOAL>μ (MeasureTheory.fundamentalFrontier G s) = 0
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Countable G<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasureTheory.IsFundamentalDomain G s μ<GOAL>μ (MeasureTheory.fundamentalInterior G s) = μ s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Countable G<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasureTheory.IsAddFundamentalDomain G s μ<GOAL>μ (MeasureTheory.addFundamentalInterior G s) = μ s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Countable G<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasureTheory.IsFundamentalDomain G s μ<VAR>MeasurableSpace G<VAR>MeasurableSMul G α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<GOAL>MeasureTheory.IsFundamentalDomain G (MeasureTheory.fundamentalInterior G s) μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>U : Set (Quotient (MulAction.orbitRel G α))<VAR>meas_U : MeasurableSet U<GOAL>(MeasureTheory.Measure.map (Quotient.mk (MulAction.orbitRel G α)) (μ.restrict s)) U = μ (Quotient.mk (MulAction.orbitRel G α) ⁻¹' U ∩ s)
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>U : Set (Quotient (AddAction.orbitRel G α))<VAR>meas_U : MeasurableSet U<GOAL>(MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (μ.restrict s)) U = μ (Quotient.mk (AddAction.orbitRel G α) ⁻¹' U ∩ s)
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable G<VAR>MeasurableSpace G<VAR>s t : Set α<VAR>MeasureTheory.SMulInvariantMeasure G α μ<VAR>MeasurableSMul G α<VAR>fund_dom_s : MeasureTheory.IsFundamentalDomain G s μ<VAR>fund_dom_t : MeasureTheory.IsFundamentalDomain G t μ<GOAL>MeasureTheory.Measure.map (Quotient.mk (MulAction.orbitRel G α)) (μ.restrict s) = MeasureTheory.Measure.map (Quotient.mk (MulAction.orbitRel G α)) (μ.restrict t)
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable G<VAR>MeasurableSpace G<VAR>s t : Set α<VAR>MeasureTheory.VAddInvariantMeasure G α μ<VAR>MeasurableVAdd G α<VAR>fund_dom_s : MeasureTheory.IsAddFundamentalDomain G s μ<VAR>fund_dom_t : MeasureTheory.IsAddFundamentalDomain G t μ<GOAL>MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (μ.restrict s) = MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (μ.restrict t)
<VAR>G : Type u_6<VAR>α : Type u_7<VAR>Zero G<VAR>VAdd G α<VAR>MeasurableSpace α<VAR>ν : autoParam (MeasureTheory.Measure α) _auto✝<VAR>self : MeasureTheory.HasAddFundamentalDomain G α ν<GOAL>∃ s, MeasureTheory.IsAddFundamentalDomain G s ν
<VAR>G : Type u_6<VAR>α : Type u_7<VAR>One G<VAR>SMul G α<VAR>MeasurableSpace α<VAR>ν : autoParam (MeasureTheory.Measure α) _auto✝<VAR>self : MeasureTheory.HasFundamentalDomain G α ν<GOAL>∃ s, MeasureTheory.IsFundamentalDomain G s ν
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>s : Set α<VAR>fund_dom_s : MeasureTheory.IsFundamentalDomain G s ν<GOAL>MeasureTheory.HasFundamentalDomain G α ν
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>s : Set α<VAR>fund_dom_s : MeasureTheory.IsAddFundamentalDomain G s ν<GOAL>MeasureTheory.HasAddFundamentalDomain G α ν
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace G<VAR>MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>Countable G<VAR>MeasurableSMul G α<VAR>MeasureTheory.SMulInvariantMeasure G α ν<VAR>s : Set α<VAR>fund_dom_s : MeasureTheory.IsFundamentalDomain G s ν<GOAL>MeasureTheory.covolume G α ν = ν s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace G<VAR>MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>Countable G<VAR>MeasurableVAdd G α<VAR>MeasureTheory.VAddInvariantMeasure G α ν<VAR>s : Set α<VAR>fund_dom_s : MeasureTheory.IsAddFundamentalDomain G s ν<GOAL>MeasureTheory.addCovolume G α ν = ν s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>ν : autoParam (MeasureTheory.Measure α) _auto✝<VAR>μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α))<VAR>self : MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ<VAR>t : Set α<GOAL>MeasureTheory.IsAddFundamentalDomain G t ν → μ = MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (MeasureTheory.Measure.restrict ν t)
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>ν : autoParam (MeasureTheory.Measure α) _auto✝<VAR>μ : MeasureTheory.Measure (Quotient (MulAction.orbitRel G α))<VAR>self : MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ<VAR>t : Set α<GOAL>MeasureTheory.IsFundamentalDomain G t ν → μ = MeasureTheory.Measure.map (Quotient.mk (MulAction.orbitRel G α)) (MeasureTheory.Measure.restrict ν t)
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>μ : MeasureTheory.Measure (Quotient (MulAction.orbitRel G α))<VAR>i : MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ<VAR>t : Set α<VAR>fund_dom_t : MeasureTheory.IsFundamentalDomain G t ν<GOAL>μ = MeasureTheory.Measure.map (Quotient.mk (MulAction.orbitRel G α)) (ν.restrict t)
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α))<VAR>i : MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ<VAR>t : Set α<VAR>fund_dom_t : MeasureTheory.IsAddFundamentalDomain G t ν<GOAL>μ = MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (ν.restrict t)
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>μ : MeasureTheory.Measure (Quotient (MulAction.orbitRel G α))<VAR>i : MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ<VAR>t : Set α<VAR>fund_dom_t : MeasureTheory.IsFundamentalDomain G t ν<VAR>U : Set (Quotient (MulAction.orbitRel G α))<VAR>meas_U : MeasurableSet U<GOAL>μ U = ν (Quotient.mk (MulAction.orbitRel G α) ⁻¹' U ∩ t)
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α))<VAR>i : MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ<VAR>t : Set α<VAR>fund_dom_t : MeasureTheory.IsAddFundamentalDomain G t ν<VAR>U : Set (Quotient (AddAction.orbitRel G α))<VAR>meas_U : MeasurableSet U<GOAL>μ U = ν (Quotient.mk (AddAction.orbitRel G α) ⁻¹' U ∩ t)
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>Countable G<VAR>MeasurableSpace G<VAR>MeasureTheory.SMulInvariantMeasure G α ν<VAR>MeasurableSMul G α<VAR>s : Set α<VAR>fund_dom_s : MeasureTheory.IsFundamentalDomain G s ν<GOAL>MeasureTheory.QuotientMeasureEqMeasurePreimage ν (MeasureTheory.Measure.map (Quotient.mk (MulAction.orbitRel G α)) (ν.restrict s))
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>Countable G<VAR>MeasurableSpace G<VAR>MeasureTheory.VAddInvariantMeasure G α ν<VAR>MeasurableVAdd G α<VAR>s : Set α<VAR>fund_dom_s : MeasureTheory.IsAddFundamentalDomain G s ν<GOAL>MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν (MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (ν.restrict s))
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>Countable G<VAR>MeasurableSpace G<VAR>MeasureTheory.VAddInvariantMeasure G α ν<VAR>MeasurableVAdd G α<VAR>μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α))<VAR>s : Set α<VAR>fund_dom_s : MeasureTheory.IsAddFundamentalDomain G s ν<VAR>h : μ = MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (ν.restrict s)<GOAL>MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>Countable G<VAR>MeasurableSpace G<VAR>MeasureTheory.SMulInvariantMeasure G α ν<VAR>MeasurableSMul G α<VAR>μ : MeasureTheory.Measure (Quotient (MulAction.orbitRel G α))<VAR>s : Set α<VAR>fund_dom_s : MeasureTheory.IsFundamentalDomain G s ν<VAR>h : μ = MeasureTheory.Measure.map (Quotient.mk (MulAction.orbitRel G α)) (ν.restrict s)<GOAL>MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>hasFun : MeasureTheory.HasFundamentalDomain G α ν<VAR>μ μ' : MeasureTheory.Measure (Quotient (MulAction.orbitRel G α))<VAR>MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ<VAR>MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ'<GOAL>μ = μ'
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>hasFun : MeasureTheory.HasAddFundamentalDomain G α ν<VAR>μ μ' : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α))<VAR>MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ<VAR>MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ'<GOAL>μ = μ'
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>𝓕 : Set α<VAR>h𝓕 : MeasureTheory.IsAddFundamentalDomain G 𝓕 ν<VAR>μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α))<VAR>MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ<GOAL>MeasureTheory.MeasurePreserving (Quotient.mk (AddAction.orbitRel G α)) (ν.restrict 𝓕) μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>𝓕 : Set α<VAR>h𝓕 : MeasureTheory.IsFundamentalDomain G 𝓕 ν<VAR>μ : MeasureTheory.Measure (Quotient (MulAction.orbitRel G α))<VAR>MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ<GOAL>MeasureTheory.MeasurePreserving (Quotient.mk (MulAction.orbitRel G α)) (ν.restrict 𝓕) μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>Countable G<VAR>MeasurableSpace G<VAR>MeasureTheory.VAddInvariantMeasure G α ν<VAR>MeasurableVAdd G α<VAR>s : Set α<VAR>fund_dom_s : MeasureTheory.IsAddFundamentalDomain G s ν<VAR>vol_s : ν s = 0<GOAL>MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν 0
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>Countable G<VAR>MeasurableSpace G<VAR>MeasureTheory.SMulInvariantMeasure G α ν<VAR>MeasurableSMul G α<VAR>s : Set α<VAR>fund_dom_s : MeasureTheory.IsFundamentalDomain G s ν<VAR>vol_s : ν s = 0<GOAL>MeasureTheory.QuotientMeasureEqMeasurePreimage ν 0
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>Countable G<VAR>MeasurableSpace G<VAR>MeasureTheory.VAddInvariantMeasure G α ν<VAR>MeasurableVAdd G α<VAR>i : MeasureTheory.SigmaFinite ν<VAR>i' : MeasureTheory.HasAddFundamentalDomain G α ν<VAR>μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α))<VAR>MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ<GOAL>MeasureTheory.SigmaFinite μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>Countable G<VAR>MeasurableSpace G<VAR>MeasureTheory.SMulInvariantMeasure G α ν<VAR>MeasurableSMul G α<VAR>i : MeasureTheory.SigmaFinite ν<VAR>i' : MeasureTheory.HasFundamentalDomain G α ν<VAR>μ : MeasureTheory.Measure (Quotient (MulAction.orbitRel G α))<VAR>MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ<GOAL>MeasureTheory.SigmaFinite μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>Countable G<VAR>MeasurableSpace G<VAR>MeasureTheory.VAddInvariantMeasure G α ν<VAR>MeasurableVAdd G α<VAR>μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α))<VAR>MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ<VAR>hasFun : MeasureTheory.HasAddFundamentalDomain G α ν<VAR>h : MeasureTheory.addCovolume G α ν ≠ ⊤<GOAL>MeasureTheory.IsFiniteMeasure μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>Countable G<VAR>MeasurableSpace G<VAR>MeasureTheory.SMulInvariantMeasure G α ν<VAR>MeasurableSMul G α<VAR>μ : MeasureTheory.Measure (Quotient (MulAction.orbitRel G α))<VAR>MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ<VAR>hasFun : MeasureTheory.HasFundamentalDomain G α ν<VAR>h : MeasureTheory.covolume G α ν ≠ ⊤<GOAL>MeasureTheory.IsFiniteMeasure μ
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>Countable G<VAR>MeasurableSpace G<VAR>MeasureTheory.SMulInvariantMeasure G α ν<VAR>MeasurableSMul G α<VAR>μ : MeasureTheory.Measure (Quotient (MulAction.orbitRel G α))<VAR>MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>MeasureTheory.covolume G α ν < ⊤
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>Countable G<VAR>MeasurableSpace G<VAR>MeasureTheory.VAddInvariantMeasure G α ν<VAR>MeasurableVAdd G α<VAR>μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α))<VAR>MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>MeasureTheory.addCovolume G α ν < ⊤
<VAR>K : semiOutParam (Type u_1)<VAR>self : RCLike K<GOAL>RCLike.re RCLike.I = 0
<VAR>K : semiOutParam (Type u_1)<VAR>self : RCLike K<VAR>r : ℝ<GOAL>RCLike.im ((algebraMap ℝ K) r) = 0
<VAR>K : semiOutParam (Type u_1)<VAR>self : RCLike K<VAR>z : K<GOAL>RCLike.im ((starRingEnd K) z) = -RCLike.im z
<VAR>K : semiOutParam (Type u_1)<VAR>self : RCLike K<VAR>r : ℝ<GOAL>RCLike.re ((algebraMap ℝ K) r) = r
<VAR>K : semiOutParam (Type u_1)<VAR>self : RCLike K<GOAL>(starRingEnd K) RCLike.I = -RCLike.I
<VAR>K : semiOutParam (Type u_1)<VAR>self : RCLike K<VAR>z : K<GOAL>‖z‖ ^ 2 = RCLike.re z * RCLike.re z + RCLike.im z * RCLike.im z
<VAR>K : semiOutParam (Type u_1)<VAR>self : RCLike K<VAR>z : K<GOAL>(algebraMap ℝ K) (RCLike.re z) + (algebraMap ℝ K) (RCLike.im z) * RCLike.I = z
<VAR>K : semiOutParam (Type u_1)<VAR>self : RCLike K<VAR>z w : K<GOAL>RCLike.re (z * w) = RCLike.re z * RCLike.re w - RCLike.im z * RCLike.im w
<VAR>K : semiOutParam (Type u_1)<VAR>self : RCLike K<VAR>z : K<GOAL>RCLike.re ((starRingEnd K) z) = RCLike.re z
<VAR>K : semiOutParam (Type u_1)<VAR>self : RCLike K<VAR>z : K<GOAL>RCLike.im z * RCLike.im RCLike.I = RCLike.im z
<VAR>K : semiOutParam (Type u_1)<VAR>self : RCLike K<GOAL>RCLike.I = 0 ∨ RCLike.I * RCLike.I = -1
<VAR>K : semiOutParam (Type u_1)<VAR>self : RCLike K<VAR>z w : K<GOAL>z ≤ w ↔ RCLike.re z ≤ RCLike.re w ∧ RCLike.im z = RCLike.im w
<VAR>K : semiOutParam (Type u_1)<VAR>self : RCLike K<VAR>z w : K<GOAL>RCLike.im (z * w) = RCLike.re z * RCLike.im w + RCLike.im z * RCLike.re w
<VAR>K : Type u_1<VAR>RCLike K<VAR>x : ℝ<GOAL>↑x = x • 1
<VAR>K : Type u_1<VAR>RCLike K<VAR>r : ℝ<VAR>z : K<GOAL>r • z = ↑r * z
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>RCLike K<VAR>AddCommGroup E<VAR>Module K E<VAR>Module ℝ E<VAR>IsScalarTower ℝ K E<VAR>r : ℝ<VAR>x : E<GOAL>r • x = ↑r • x
<VAR>K : Type u_1<VAR>RCLike K<GOAL>⇑(algebraMap ℝ K) = RCLike.ofReal
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>↑(RCLike.re z) + ↑(RCLike.im z) * RCLike.I = z
<VAR>K : Type u_1<VAR>RCLike K<VAR>r : ℝ<GOAL>RCLike.re ↑r = r
<VAR>K : Type u_1<VAR>RCLike K<VAR>r : ℝ<GOAL>RCLike.im ↑r = 0
<VAR>K : Type u_1<VAR>RCLike K<VAR>z w : K<GOAL>RCLike.re (z * w) = RCLike.re z * RCLike.re w - RCLike.im z * RCLike.im w
<VAR>K : Type u_1<VAR>RCLike K<VAR>z w : K<GOAL>RCLike.im (z * w) = RCLike.re z * RCLike.im w + RCLike.im z * RCLike.re w
<VAR>K : Type u_1<VAR>RCLike K<VAR>z w : K<GOAL>z = w ↔ RCLike.re z = RCLike.re w ∧ RCLike.im z = RCLike.im w
<VAR>K : Type u_1<VAR>RCLike K<VAR>z w : K<VAR>hre : RCLike.re z = RCLike.re w<VAR>him : RCLike.im z = RCLike.im w<GOAL>z = w
<VAR>K : Type u_1<VAR>RCLike K<GOAL>↑0 = 0
<VAR>K : Type u_1<VAR>RCLike K<GOAL>RCLike.re 0 = 0
<VAR>K : Type u_1<VAR>RCLike K<GOAL>↑1 = 1
<VAR>K : Type u_1<VAR>RCLike K<GOAL>RCLike.re 1 = 1
<VAR>K : Type u_1<VAR>RCLike K<GOAL>RCLike.im 1 = 0
<VAR>K : Type u_1<VAR>RCLike K<GOAL>Function.Injective RCLike.ofReal
<VAR>K : Type u_1<VAR>RCLike K<VAR>z w : ℝ<GOAL>↑z = ↑w ↔ z = w
<VAR>K : Type u_1<VAR>RCLike K<VAR>x : ℝ<GOAL>↑x = 0 ↔ x = 0
<VAR>K : Type u_1<VAR>RCLike K<VAR>x : ℝ<GOAL>↑x ≠ 0 ↔ x ≠ 0
<VAR>K : Type u_1<VAR>RCLike K<VAR>r s : ℝ<GOAL>↑(r + s) = ↑r + ↑s
<VAR>K : Type u_1<VAR>RCLike K<VAR>r : ℝ<GOAL>↑(-r) = -↑r
<VAR>K : Type u_1<VAR>RCLike K<VAR>r s : ℝ<GOAL>↑(r - s) = ↑r - ↑s
<VAR>K : Type u_1<VAR>RCLike K<VAR>α : Type u_3<VAR>s : Finset α<VAR>f : α → ℝ<GOAL>↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
<VAR>K : Type u_1<VAR>RCLike K<VAR>α : Type u_3<VAR>M : Type u_4<VAR>Zero M<VAR>f : α →₀ M<VAR>g : α → M → ℝ<GOAL>↑(f.sum fun a b => g a b) = f.sum fun a b => ↑(g a b)
<VAR>K : Type u_1<VAR>RCLike K<VAR>r s : ℝ<GOAL>↑(r * s) = ↑r * ↑s
<VAR>K : Type u_1<VAR>RCLike K<VAR>r : ℝ<VAR>n : ℕ<GOAL>↑(r ^ n) = ↑r ^ n
<VAR>K : Type u_1<VAR>RCLike K<VAR>α : Type u_3<VAR>s : Finset α<VAR>f : α → ℝ<GOAL>↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
<VAR>K : Type u_1<VAR>RCLike K<VAR>α : Type u_3<VAR>M : Type u_4<VAR>Zero M<VAR>f : α →₀ M<VAR>g : α → M → ℝ<GOAL>↑(f.prod fun a b => g a b) = f.prod fun a b => ↑(g a b)
<VAR>K : Type u_1<VAR>RCLike K<VAR>r x : ℝ<GOAL>r • ↑x = ↑r * ↑x
<VAR>K : Type u_1<VAR>RCLike K<VAR>r : ℝ<VAR>z : K<GOAL>RCLike.re (↑r * z) = r * RCLike.re z
<VAR>K : Type u_1<VAR>RCLike K<VAR>r : ℝ<VAR>z : K<GOAL>RCLike.im (↑r * z) = r * RCLike.im z
<VAR>K : Type u_1<VAR>RCLike K<VAR>r : ℝ<VAR>z : K<GOAL>RCLike.re (r • z) = r * RCLike.re z
<VAR>K : Type u_1<VAR>RCLike K<VAR>r : ℝ<VAR>z : K<GOAL>RCLike.im (r • z) = r * RCLike.im z
<VAR>K : Type u_1<VAR>RCLike K<VAR>r : ℝ<GOAL>‖↑r‖ = |r|
<VAR>K : Type u_1<VAR>RCLike K<GOAL>RCLike.re RCLike.I = 0
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>RCLike.im z * RCLike.im RCLike.I = RCLike.im z
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>RCLike.im RCLike.I * RCLike.im z = RCLike.im z
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>RCLike.re (RCLike.I * z) = -RCLike.im z
<VAR>K : Type u_1<VAR>RCLike K<GOAL>RCLike.I = 0 ∨ RCLike.I * RCLike.I = -1
<VAR>K : Type u_1<VAR>RCLike K<GOAL>RCLike.I = 0 ∨ RCLike.im RCLike.I = 1
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>RCLike.re ((starRingEnd K) z) = RCLike.re z
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>RCLike.im ((starRingEnd K) z) = -RCLike.im z
<VAR>K : Type u_1<VAR>RCLike K<GOAL>(starRingEnd K) RCLike.I = -RCLike.I
<VAR>K : Type u_1<VAR>RCLike K<VAR>r : ℝ<GOAL>(starRingEnd K) ↑r = ↑r
<VAR>K : Type u_1<VAR>RCLike K<VAR>n : ℕ<GOAL>(starRingEnd K) ↑n = ↑n
<VAR>K : Type u_1<VAR>RCLike K<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>(starRingEnd K) (OfNat.ofNat n) = OfNat.ofNat n
<VAR>K : Type u_1<VAR>RCLike K<GOAL>(starRingEnd K) (-RCLike.I) = RCLike.I
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>(starRingEnd K) z = ↑(RCLike.re z) - ↑(RCLike.im z) * RCLike.I
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>z - (starRingEnd K) z = 2 * ↑(RCLike.im z) * RCLike.I
<VAR>K : Type u_1<VAR>RCLike K<VAR>r : ℝ<VAR>z : K<GOAL>(starRingEnd K) (r • z) = r • (starRingEnd K) z
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>z + (starRingEnd K) z = 2 * ↑(RCLike.re z)
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>↑(RCLike.re z) = (z + (starRingEnd K) z) / 2
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>↑(RCLike.im z) = RCLike.I * ((starRingEnd K) z - z) / 2
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>[(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(RCLike.re z) = z, RCLike.im z = 0].TFAE
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>(starRingEnd K) z = z ↔ ∃ r, z = ↑r
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>(starRingEnd K) z = z ↔ ↑(RCLike.re z) = z
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>(starRingEnd K) z = z ↔ RCLike.im z = 0
<VAR>K : Type u_1<VAR>RCLike K<GOAL>star = ⇑(starRingEnd K)
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>RCLike.normSq z = RCLike.re z * RCLike.re z + RCLike.im z * RCLike.im z
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>‖z‖ ^ 2 = RCLike.re z * RCLike.re z + RCLike.im z * RCLike.im z
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>RCLike.normSq z = ‖z‖ ^ 2
<VAR>K : Type u_1<VAR>RCLike K<GOAL>RCLike.normSq 0 = 0
<VAR>K : Type u_1<VAR>RCLike K<GOAL>RCLike.normSq 1 = 1
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>0 ≤ RCLike.normSq z
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>RCLike.normSq z = 0 ↔ z = 0
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>0 < RCLike.normSq z ↔ z ≠ 0
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>RCLike.normSq (-z) = RCLike.normSq z
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>RCLike.normSq ((starRingEnd K) z) = RCLike.normSq z
<VAR>K : Type u_1<VAR>RCLike K<VAR>z w : K<GOAL>RCLike.normSq (z * w) = RCLike.normSq z * RCLike.normSq w
<VAR>K : Type u_1<VAR>RCLike K<VAR>z w : K<GOAL>RCLike.normSq (z + w) = RCLike.normSq z + RCLike.normSq w + 2 * RCLike.re (z * (starRingEnd K) w)
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>RCLike.re z * RCLike.re z ≤ RCLike.normSq z
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>RCLike.im z * RCLike.im z ≤ RCLike.normSq z
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>z * (starRingEnd K) z = ↑‖z‖ ^ 2
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>(starRingEnd K) z * z = ↑‖z‖ ^ 2
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<VAR>hz : ‖z‖ = 1<GOAL>z⁻¹ = (starRingEnd K) z
<VAR>K : Type u_1<VAR>RCLike K<VAR>z w : K<GOAL>RCLike.normSq (z - w) = RCLike.normSq z + RCLike.normSq w - 2 * RCLike.re (z * (starRingEnd K) w)
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>√(RCLike.normSq z) = ‖z‖
<VAR>K : Type u_1<VAR>RCLike K<VAR>r : ℝ<GOAL>↑r⁻¹ = (↑r)⁻¹
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>z⁻¹ = (starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>RCLike.re z⁻¹ = RCLike.re z / RCLike.normSq z
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>RCLike.im z⁻¹ = -RCLike.im z / RCLike.normSq z
<VAR>K : Type u_1<VAR>RCLike K<VAR>z w : K<GOAL>RCLike.re (z / w) = RCLike.re z * RCLike.re w / RCLike.normSq w + RCLike.im z * RCLike.im w / RCLike.normSq w
<VAR>K : Type u_1<VAR>RCLike K<VAR>z w : K<GOAL>RCLike.im (z / w) = RCLike.im z * RCLike.re w / RCLike.normSq w - RCLike.re z * RCLike.im w / RCLike.normSq w
<VAR>K : Type u_1<VAR>RCLike K<VAR>x : K<GOAL>(starRingEnd K) x⁻¹ = ((starRingEnd K) x)⁻¹