ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>b : ℂ<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>FiniteDimensional ℝ V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>w : V<GOAL>∫ (v : V), cexp (-b * ↑‖v‖ ^ 2 + c * ↑⟪w, v⟫_ℝ) = (↑π / b) ^ (↑(FiniteDimensional.finrank ℝ V) / 2) * cexp (c ^ 2 * ↑‖w‖ ^ 2 / (4 * b))
<VAR>b : ℂ<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>FiniteDimensional ℝ V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>hb : 0 < b.re<GOAL>∫ (v : V), cexp (-b * ↑‖v‖ ^ 2) = (↑π / b) ^ (↑(FiniteDimensional.finrank ℝ V) / 2)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>FiniteDimensional ℝ V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>b : ℝ<VAR>hb : 0 < b<GOAL>∫ (v : V), rexp (-b * ‖v‖ ^ 2) = (π / b) ^ (↑(FiniteDimensional.finrank ℝ V) / 2)
<VAR>b : ℂ<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>FiniteDimensional ℝ V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>hb : 0 < b.re<VAR>x w : V<GOAL>𝓕 (fun v => cexp (-b * ↑‖v‖ ^ 2 + 2 * ↑π * Complex.I * ↑⟪x, v⟫_ℝ)) w = (↑π / b) ^ (↑(FiniteDimensional.finrank ℝ V) / 2) * cexp (-↑π ^ 2 * ↑‖x - w‖ ^ 2 / b)
<VAR>b : ℂ<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>FiniteDimensional ℝ V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>hb : 0 < b.re<VAR>w : V<GOAL>𝓕 (fun v => cexp (-b * ↑‖v‖ ^ 2)) w = (↑π / b) ^ (↑(FiniteDimensional.finrank ℝ V) / 2) * cexp (-↑π ^ 2 * ↑‖w‖ ^ 2 / b)
<VAR>𝕜 : Type u_1<VAR>R : Type u_2<VAR>Field 𝕜<VAR>CharZero 𝕜<VAR>CommRing R<VAR>Algebra 𝕜 R<VAR>UniformSpace R<VAR>TopologicalRing R<VAR>T2Space R<GOAL>NormedSpace.exp 𝕜 DualNumber.eps = 1 + DualNumber.eps
<VAR>𝕜 : Type u_1<VAR>R : Type u_2<VAR>Field 𝕜<VAR>CharZero 𝕜<VAR>CommRing R<VAR>Algebra 𝕜 R<VAR>UniformSpace R<VAR>TopologicalRing R<VAR>T2Space R<VAR>r : R<GOAL>NormedSpace.exp 𝕜 (r • DualNumber.eps) = 1 + r • DualNumber.eps
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>𝔸 : Type u_6<VAR>Fintype m<VAR>DecidableEq m<VAR>Field 𝕂<VAR>Ring 𝔸<VAR>TopologicalSpace 𝔸<VAR>TopologicalRing 𝔸<VAR>Algebra 𝕂 𝔸<VAR>T2Space 𝔸<VAR>v : m → 𝔸<GOAL>NormedSpace.exp 𝕂 (Matrix.diagonal v) = Matrix.diagonal (NormedSpace.exp 𝕂 v)
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>𝔸 : Type u_6<VAR>Fintype m<VAR>DecidableEq m<VAR>Fintype n<VAR>DecidableEq n<VAR>Field 𝕂<VAR>Ring 𝔸<VAR>TopologicalSpace 𝔸<VAR>TopologicalRing 𝔸<VAR>Algebra 𝕂 𝔸<VAR>T2Space 𝔸<VAR>v : m → Matrix n n 𝔸<GOAL>NormedSpace.exp 𝕂 (Matrix.blockDiagonal v) = Matrix.blockDiagonal (NormedSpace.exp 𝕂 v)
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>n' : m → Type u_5<VAR>𝔸 : Type u_6<VAR>Fintype m<VAR>DecidableEq m<VAR>(i : m) → Fintype (n' i)<VAR>(i : m) → DecidableEq (n' i)<VAR>Field 𝕂<VAR>Ring 𝔸<VAR>TopologicalSpace 𝔸<VAR>TopologicalRing 𝔸<VAR>Algebra 𝕂 𝔸<VAR>T2Space 𝔸<VAR>v : (i : m) → Matrix (n' i) (n' i) 𝔸<GOAL>NormedSpace.exp 𝕂 (Matrix.blockDiagonal' v) = Matrix.blockDiagonal' (NormedSpace.exp 𝕂 v)
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>𝔸 : Type u_6<VAR>Fintype m<VAR>DecidableEq m<VAR>Field 𝕂<VAR>Ring 𝔸<VAR>TopologicalSpace 𝔸<VAR>TopologicalRing 𝔸<VAR>Algebra 𝕂 𝔸<VAR>T2Space 𝔸<VAR>StarRing 𝔸<VAR>ContinuousStar 𝔸<VAR>A : Matrix m m 𝔸<GOAL>NormedSpace.exp 𝕂 Aᴴ = (NormedSpace.exp 𝕂 A)ᴴ
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>𝔸 : Type u_6<VAR>Fintype m<VAR>DecidableEq m<VAR>Field 𝕂<VAR>Ring 𝔸<VAR>TopologicalSpace 𝔸<VAR>TopologicalRing 𝔸<VAR>Algebra 𝕂 𝔸<VAR>T2Space 𝔸<VAR>StarRing 𝔸<VAR>ContinuousStar 𝔸<VAR>A : Matrix m m 𝔸<VAR>h : A.IsHermitian<GOAL>(NormedSpace.exp 𝕂 A).IsHermitian
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>𝔸 : Type u_6<VAR>Fintype m<VAR>DecidableEq m<VAR>Field 𝕂<VAR>CommRing 𝔸<VAR>TopologicalSpace 𝔸<VAR>TopologicalRing 𝔸<VAR>Algebra 𝕂 𝔸<VAR>T2Space 𝔸<VAR>A : Matrix m m 𝔸<GOAL>NormedSpace.exp 𝕂 Aᵀ = (NormedSpace.exp 𝕂 A)ᵀ
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>𝔸 : Type u_6<VAR>Fintype m<VAR>DecidableEq m<VAR>Field 𝕂<VAR>CommRing 𝔸<VAR>TopologicalSpace 𝔸<VAR>TopologicalRing 𝔸<VAR>Algebra 𝕂 𝔸<VAR>T2Space 𝔸<VAR>A : Matrix m m 𝔸<VAR>h : A.IsSymm<GOAL>(NormedSpace.exp 𝕂 A).IsSymm
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>𝔸 : Type u_6<VAR>RCLike 𝕂<VAR>Fintype m<VAR>DecidableEq m<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>A B : Matrix m m 𝔸<VAR>h : Commute A B<GOAL>NormedSpace.exp 𝕂 (A + B) = NormedSpace.exp 𝕂 A * NormedSpace.exp 𝕂 B
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>𝔸 : Type u_6<VAR>RCLike 𝕂<VAR>Fintype m<VAR>DecidableEq m<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>ι : Type u_7<VAR>s : Finset ι<VAR>f : ι → Matrix m m 𝔸<VAR>h : (↑s).Pairwise fun i j => Commute (f i) (f j)<GOAL>NormedSpace.exp 𝕂 (∑ i ∈ s, f i) = s.noncommProd (fun i => NormedSpace.exp 𝕂 (f i)) ⋯
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>𝔸 : Type u_6<VAR>RCLike 𝕂<VAR>Fintype m<VAR>DecidableEq m<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>n : ℕ<VAR>A : Matrix m m 𝔸<GOAL>NormedSpace.exp 𝕂 (n • A) = NormedSpace.exp 𝕂 A ^ n
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>𝔸 : Type u_6<VAR>RCLike 𝕂<VAR>Fintype m<VAR>DecidableEq m<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>A : Matrix m m 𝔸<GOAL>IsUnit (NormedSpace.exp 𝕂 A)
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>𝔸 : Type u_6<VAR>RCLike 𝕂<VAR>Fintype m<VAR>DecidableEq m<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>U : (Matrix m m 𝔸)ˣ<VAR>A : Matrix m m 𝔸<GOAL>NormedSpace.exp 𝕂 (↑U * A * ↑U⁻¹) = ↑U * NormedSpace.exp 𝕂 A * ↑U⁻¹
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>𝔸 : Type u_6<VAR>RCLike 𝕂<VAR>Fintype m<VAR>DecidableEq m<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>U : (Matrix m m 𝔸)ˣ<VAR>A : Matrix m m 𝔸<GOAL>NormedSpace.exp 𝕂 (↑U⁻¹ * A * ↑U) = ↑U⁻¹ * NormedSpace.exp 𝕂 A * ↑U
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>𝔸 : Type u_6<VAR>RCLike 𝕂<VAR>Fintype m<VAR>DecidableEq m<VAR>NormedCommRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>A : Matrix m m 𝔸<GOAL>NormedSpace.exp 𝕂 (-A) = (NormedSpace.exp 𝕂 A)⁻¹
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>𝔸 : Type u_6<VAR>RCLike 𝕂<VAR>Fintype m<VAR>DecidableEq m<VAR>NormedCommRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>z : ℤ<VAR>A : Matrix m m 𝔸<GOAL>NormedSpace.exp 𝕂 (z • A) = NormedSpace.exp 𝕂 A ^ z
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>𝔸 : Type u_6<VAR>RCLike 𝕂<VAR>Fintype m<VAR>DecidableEq m<VAR>NormedCommRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>U A : Matrix m m 𝔸<VAR>hy : IsUnit U<GOAL>NormedSpace.exp 𝕂 (U * A * U⁻¹) = U * NormedSpace.exp 𝕂 A * U⁻¹
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>𝔸 : Type u_6<VAR>RCLike 𝕂<VAR>Fintype m<VAR>DecidableEq m<VAR>NormedCommRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>U A : Matrix m m 𝔸<VAR>hy : IsUnit U<GOAL>NormedSpace.exp 𝕂 (U⁻¹ * A * U) = U⁻¹ * NormedSpace.exp 𝕂 A * U
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>Field 𝕂<VAR>Ring 𝔸<VAR>Algebra 𝕂 𝔸<VAR>TopologicalSpace 𝔸<VAR>TopologicalRing 𝔸<VAR>x : 𝔸<VAR>n : ℕ<GOAL>((NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x) = (↑n.factorial)⁻¹ • x ^ n
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>Field 𝕂<VAR>Ring 𝔸<VAR>Algebra 𝕂 𝔸<VAR>TopologicalSpace 𝔸<VAR>TopologicalRing 𝔸<VAR>x : 𝔸<GOAL>(fun n => (NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x) = fun n => (↑n.factorial)⁻¹ • x ^ n
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>Field 𝕂<VAR>Ring 𝔸<VAR>Algebra 𝕂 𝔸<VAR>TopologicalSpace 𝔸<VAR>TopologicalRing 𝔸<VAR>x : 𝔸<GOAL>(NormedSpace.expSeries 𝕂 𝔸).sum x = ∑' (n : ℕ), (↑n.factorial)⁻¹ • x ^ n
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>Field 𝕂<VAR>Ring 𝔸<VAR>Algebra 𝕂 𝔸<VAR>TopologicalSpace 𝔸<VAR>TopologicalRing 𝔸<GOAL>NormedSpace.exp 𝕂 = fun x => ∑' (n : ℕ), (↑n.factorial)⁻¹ • x ^ n
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>Field 𝕂<VAR>Ring 𝔸<VAR>Algebra 𝕂 𝔸<VAR>TopologicalSpace 𝔸<VAR>TopologicalRing 𝔸<VAR>n : ℕ<GOAL>((NormedSpace.expSeries 𝕂 𝔸 n) fun x => 0) = Pi.single 0 1 n
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>Field 𝕂<VAR>Ring 𝔸<VAR>Algebra 𝕂 𝔸<VAR>TopologicalSpace 𝔸<VAR>TopologicalRing 𝔸<GOAL>NormedSpace.exp 𝕂 0 = 1
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>Field 𝕂<VAR>Ring 𝔸<VAR>Algebra 𝕂 𝔸<VAR>TopologicalSpace 𝔸<VAR>TopologicalRing 𝔸<VAR>T2Space 𝔸<VAR>x : 𝔸<GOAL>NormedSpace.exp 𝕂 (MulOpposite.op x) = MulOpposite.op (NormedSpace.exp 𝕂 x)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>Field 𝕂<VAR>Ring 𝔸<VAR>Algebra 𝕂 𝔸<VAR>TopologicalSpace 𝔸<VAR>TopologicalRing 𝔸<VAR>T2Space 𝔸<VAR>x : 𝔸ᵐᵒᵖ<GOAL>NormedSpace.exp 𝕂 (MulOpposite.unop x) = MulOpposite.unop (NormedSpace.exp 𝕂 x)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>Field 𝕂<VAR>Ring 𝔸<VAR>Algebra 𝕂 𝔸<VAR>TopologicalSpace 𝔸<VAR>TopologicalRing 𝔸<VAR>T2Space 𝔸<VAR>StarRing 𝔸<VAR>ContinuousStar 𝔸<VAR>x : 𝔸<GOAL>star (NormedSpace.exp 𝕂 x) = NormedSpace.exp 𝕂 (star x)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>Field 𝕂<VAR>Ring 𝔸<VAR>Algebra 𝕂 𝔸<VAR>TopologicalSpace 𝔸<VAR>TopologicalRing 𝔸<VAR>T2Space 𝔸<VAR>StarRing 𝔸<VAR>ContinuousStar 𝔸<VAR>x : 𝔸<VAR>h : IsSelfAdjoint x<GOAL>IsSelfAdjoint (NormedSpace.exp 𝕂 x)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>Field 𝕂<VAR>Ring 𝔸<VAR>Algebra 𝕂 𝔸<VAR>TopologicalSpace 𝔸<VAR>TopologicalRing 𝔸<VAR>T2Space 𝔸<VAR>x y : 𝔸<VAR>h : Commute x y<GOAL>Commute x (NormedSpace.exp 𝕂 y)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>Field 𝕂<VAR>Ring 𝔸<VAR>Algebra 𝕂 𝔸<VAR>TopologicalSpace 𝔸<VAR>TopologicalRing 𝔸<VAR>T2Space 𝔸<VAR>x y : 𝔸<VAR>h : Commute x y<GOAL>Commute (NormedSpace.exp 𝕂 x) y
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>Field 𝕂<VAR>Ring 𝔸<VAR>Algebra 𝕂 𝔸<VAR>TopologicalSpace 𝔸<VAR>TopologicalRing 𝔸<VAR>T2Space 𝔸<VAR>x y : 𝔸<VAR>h : Commute x y<GOAL>Commute (NormedSpace.exp 𝕂 x) (NormedSpace.exp 𝕂 y)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>Field 𝕂<VAR>DivisionRing 𝔸<VAR>Algebra 𝕂 𝔸<VAR>TopologicalSpace 𝔸<VAR>TopologicalRing 𝔸<VAR>x : 𝔸<VAR>n : ℕ<GOAL>((NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x) = x ^ n / ↑n.factorial
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>Field 𝕂<VAR>DivisionRing 𝔸<VAR>Algebra 𝕂 𝔸<VAR>TopologicalSpace 𝔸<VAR>TopologicalRing 𝔸<VAR>x : 𝔸<GOAL>(fun n => (NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x) = fun n => x ^ n / ↑n.factorial
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>Field 𝕂<VAR>DivisionRing 𝔸<VAR>Algebra 𝕂 𝔸<VAR>TopologicalSpace 𝔸<VAR>TopologicalRing 𝔸<VAR>x : 𝔸<GOAL>(NormedSpace.expSeries 𝕂 𝔸).sum x = ∑' (n : ℕ), x ^ n / ↑n.factorial
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>Field 𝕂<VAR>DivisionRing 𝔸<VAR>Algebra 𝕂 𝔸<VAR>TopologicalSpace 𝔸<VAR>TopologicalRing 𝔸<GOAL>NormedSpace.exp 𝕂 = fun x => ∑' (n : ℕ), x ^ n / ↑n.factorial
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>NontriviallyNormedField 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius<GOAL>Summable fun n => ‖(NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x‖
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>NontriviallyNormedField 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius<GOAL>Summable fun n => ‖(↑n.factorial)⁻¹ • x ^ n‖
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>NontriviallyNormedField 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius<GOAL>Summable fun n => (NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>NontriviallyNormedField 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius<GOAL>Summable fun n => (↑n.factorial)⁻¹ • x ^ n
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>NontriviallyNormedField 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius<GOAL>HasSum (fun n => (NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x) (NormedSpace.exp 𝕂 x)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>NontriviallyNormedField 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius<GOAL>HasSum (fun n => (↑n.factorial)⁻¹ • x ^ n) (NormedSpace.exp 𝕂 x)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>NontriviallyNormedField 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>h : 0 < (NormedSpace.expSeries 𝕂 𝔸).radius<GOAL>HasFPowerSeriesOnBall (NormedSpace.exp 𝕂) (NormedSpace.expSeries 𝕂 𝔸) 0 (NormedSpace.expSeries 𝕂 𝔸).radius
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>NontriviallyNormedField 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>h : 0 < (NormedSpace.expSeries 𝕂 𝔸).radius<GOAL>HasFPowerSeriesAt (NormedSpace.exp 𝕂) (NormedSpace.expSeries 𝕂 𝔸) 0
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>NontriviallyNormedField 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<GOAL>ContinuousOn (NormedSpace.exp 𝕂) (EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>NontriviallyNormedField 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius<GOAL>AnalyticAt 𝕂 (NormedSpace.exp 𝕂) x
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>NontriviallyNormedField 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>CharZero 𝕂<VAR>x y : 𝔸<VAR>hxy : Commute x y<VAR>hx : x ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius<VAR>hy : y ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius<GOAL>NormedSpace.exp 𝕂 (x + y) = NormedSpace.exp 𝕂 x * NormedSpace.exp 𝕂 y
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>NontriviallyNormedField 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>CharZero 𝕂<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius<GOAL>IsUnit (NormedSpace.exp 𝕂 x)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>NontriviallyNormedField 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>CharZero 𝕂<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius<VAR>Invertible (NormedSpace.exp 𝕂 x)<GOAL>⅟(NormedSpace.exp 𝕂 x) = NormedSpace.exp 𝕂 (-x)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>NontriviallyNormedField 𝕂<VAR>NormedRing 𝔸<VAR>NormedRing 𝔹<VAR>NormedAlgebra 𝕂 𝔸<VAR>NormedAlgebra 𝕂 𝔹<VAR>CompleteSpace 𝔸<VAR>F : Type u_4<VAR>FunLike F 𝔸 𝔹<VAR>RingHomClass F 𝔸 𝔹<VAR>f : F<VAR>hf : Continuous ⇑f<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius<GOAL>f (NormedSpace.exp 𝕂 x) = NormedSpace.exp 𝕂 (f x)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>NontriviallyNormedField 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝕂<VAR>x : 𝕂<VAR>hx : x ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝕂).radius<GOAL>(algebraMap 𝕂 𝔸) (NormedSpace.exp 𝕂 x) = NormedSpace.exp 𝕂 ((algebraMap 𝕂 𝔸) x)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>NontriviallyNormedField 𝕂<VAR>NormedDivisionRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius<GOAL>Summable fun n => ‖x ^ n / ↑n.factorial‖
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>NontriviallyNormedField 𝕂<VAR>NormedDivisionRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius<GOAL>Summable fun n => x ^ n / ↑n.factorial
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>NontriviallyNormedField 𝕂<VAR>NormedDivisionRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius<GOAL>HasSum (fun n => x ^ n / ↑n.factorial) (NormedSpace.exp 𝕂 x)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>NontriviallyNormedField 𝕂<VAR>NormedDivisionRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CharZero 𝕂<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius<GOAL>NormedSpace.exp 𝕂 (-x) = (NormedSpace.exp 𝕂 x)⁻¹
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>NontriviallyNormedField 𝕂<VAR>NormedCommRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>CharZero 𝕂<VAR>x y : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius<VAR>hy : y ∈ EMetric.ball 0 (NormedSpace.expSeries 𝕂 𝔸).radius<GOAL>NormedSpace.exp 𝕂 (x + y) = NormedSpace.exp 𝕂 x * NormedSpace.exp 𝕂 y
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<GOAL>(NormedSpace.expSeries 𝕂 𝔸).radius = ⊤
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<GOAL>0 < (NormedSpace.expSeries 𝕂 𝔸).radius
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>x : 𝔸<GOAL>Summable fun n => ‖(NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x‖
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>x : 𝔸<GOAL>Summable fun n => ‖(↑n.factorial)⁻¹ • x ^ n‖
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<GOAL>Summable fun n => (NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<GOAL>Summable fun n => (↑n.factorial)⁻¹ • x ^ n
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<GOAL>HasSum (fun n => (NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x) (NormedSpace.exp 𝕂 x)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<GOAL>HasSum (fun n => (↑n.factorial)⁻¹ • x ^ n) (NormedSpace.exp 𝕂 x)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<GOAL>HasFPowerSeriesOnBall (NormedSpace.exp 𝕂) (NormedSpace.expSeries 𝕂 𝔸) 0 ⊤
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<GOAL>HasFPowerSeriesAt (NormedSpace.exp 𝕂) (NormedSpace.expSeries 𝕂 𝔸) 0
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<GOAL>Continuous (NormedSpace.exp 𝕂)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>α : Type u_4<VAR>l : Filter α<VAR>f : α → 𝔸<VAR>a : 𝔸<VAR>hf : Filter.Tendsto f l (nhds a)<GOAL>Filter.Tendsto (fun x => NormedSpace.exp 𝕂 (f x)) l (nhds (NormedSpace.exp 𝕂 a))
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<GOAL>AnalyticAt 𝕂 (NormedSpace.exp 𝕂) x
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>x y : 𝔸<VAR>hxy : Commute x y<GOAL>NormedSpace.exp 𝕂 (x + y) = NormedSpace.exp 𝕂 x * NormedSpace.exp 𝕂 y
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<GOAL>IsUnit (NormedSpace.exp 𝕂 x)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<VAR>Invertible (NormedSpace.exp 𝕂 x)<GOAL>⅟(NormedSpace.exp 𝕂 x) = NormedSpace.exp 𝕂 (-x)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<GOAL>Ring.inverse (NormedSpace.exp 𝕂 x) = NormedSpace.exp 𝕂 (-x)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>StarRing 𝔸<VAR>ContinuousStar 𝔸<VAR>x : 𝔸<VAR>h : x ∈ skewAdjoint 𝔸<GOAL>NormedSpace.exp 𝕂 x ∈ unitary 𝔸
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>f : ι → 𝔸<VAR>h : (↑s).Pairwise fun i j => Commute (f i) (f j)<GOAL>NormedSpace.exp 𝕂 (∑ i ∈ s, f i) = s.noncommProd (fun i => NormedSpace.exp 𝕂 (f i)) ⋯
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>n : ℕ<VAR>x : 𝔸<GOAL>NormedSpace.exp 𝕂 (n • x) = NormedSpace.exp 𝕂 x ^ n
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>NormedRing 𝔹<VAR>NormedAlgebra 𝕂 𝔹<VAR>CompleteSpace 𝔸<VAR>F : Type u_4<VAR>FunLike F 𝔸 𝔹<VAR>RingHomClass F 𝔸 𝔹<VAR>f : F<VAR>hf : Continuous ⇑f<VAR>x : 𝔸<GOAL>f (NormedSpace.exp 𝕂 x) = NormedSpace.exp 𝕂 (f x)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>G : Type u_4<VAR>Monoid G<VAR>MulSemiringAction G 𝔸<VAR>ContinuousConstSMul G 𝔸<VAR>g : G<VAR>x : 𝔸<GOAL>NormedSpace.exp 𝕂 (g • x) = g • NormedSpace.exp 𝕂 x
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>y : 𝔸ˣ<VAR>x : 𝔸<GOAL>NormedSpace.exp 𝕂 (↑y * x * ↑y⁻¹) = ↑y * NormedSpace.exp 𝕂 x * ↑y⁻¹
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>y : 𝔸ˣ<VAR>x : 𝔸<GOAL>NormedSpace.exp 𝕂 (↑y⁻¹ * x * ↑y) = ↑y⁻¹ * NormedSpace.exp 𝕂 x * ↑y
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>NormedRing 𝔹<VAR>NormedAlgebra 𝕂 𝔹<VAR>CompleteSpace 𝔸<VAR>CompleteSpace 𝔹<VAR>x : 𝔸 × 𝔹<GOAL>(NormedSpace.exp 𝕂 x).1 = NormedSpace.exp 𝕂 x.1
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>NormedRing 𝔹<VAR>NormedAlgebra 𝕂 𝔹<VAR>CompleteSpace 𝔸<VAR>CompleteSpace 𝔹<VAR>x : 𝔸 × 𝔹<GOAL>(NormedSpace.exp 𝕂 x).2 = NormedSpace.exp 𝕂 x.2
<VAR>𝕂 : Type u_1<VAR>RCLike 𝕂<VAR>ι : Type u_4<VAR>𝔸 : ι → Type u_5<VAR>Finite ι<VAR>(i : ι) → NormedRing (𝔸 i)<VAR>(i : ι) → NormedAlgebra 𝕂 (𝔸 i)<VAR>∀ (i : ι), CompleteSpace (𝔸 i)<VAR>x : (i : ι) → 𝔸 i<VAR>i : ι<GOAL>NormedSpace.exp 𝕂 x i = NormedSpace.exp 𝕂 (x i)
<VAR>𝕂 : Type u_1<VAR>RCLike 𝕂<VAR>ι : Type u_4<VAR>𝔸 : ι → Type u_5<VAR>Finite ι<VAR>(i : ι) → NormedRing (𝔸 i)<VAR>(i : ι) → NormedAlgebra 𝕂 (𝔸 i)<VAR>∀ (i : ι), CompleteSpace (𝔸 i)<VAR>x : (i : ι) → 𝔸 i<GOAL>NormedSpace.exp 𝕂 x = fun i => NormedSpace.exp 𝕂 (x i)
<VAR>𝕂 : Type u_1<VAR>RCLike 𝕂<VAR>ι : Type u_4<VAR>𝔸 : ι → Type u_5<VAR>Finite ι<VAR>DecidableEq ι<VAR>(i : ι) → NormedRing (𝔸 i)<VAR>(i : ι) → NormedAlgebra 𝕂 (𝔸 i)<VAR>∀ (i : ι), CompleteSpace (𝔸 i)<VAR>x : (i : ι) → 𝔸 i<VAR>j : ι<VAR>xj : 𝔸 j<GOAL>Function.update (NormedSpace.exp 𝕂 x) j (NormedSpace.exp 𝕂 xj) = NormedSpace.exp 𝕂 (Function.update x j xj)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>x : 𝕂<GOAL>(algebraMap 𝕂 𝔸) (NormedSpace.exp 𝕂 x) = NormedSpace.exp 𝕂 ((algebraMap 𝕂 𝔸) x)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedDivisionRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>x : 𝔸<GOAL>Summable fun n => ‖x ^ n / ↑n.factorial‖
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedDivisionRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<GOAL>Summable fun n => x ^ n / ↑n.factorial
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedDivisionRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<GOAL>HasSum (fun n => x ^ n / ↑n.factorial) (NormedSpace.exp 𝕂 x)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedDivisionRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>x : 𝔸<GOAL>NormedSpace.exp 𝕂 (-x) = (NormedSpace.exp 𝕂 x)⁻¹
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedDivisionRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>z : ℤ<VAR>x : 𝔸<GOAL>NormedSpace.exp 𝕂 (z • x) = NormedSpace.exp 𝕂 x ^ z
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedDivisionRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>y x : 𝔸<VAR>hy : y ≠ 0<GOAL>NormedSpace.exp 𝕂 (y * x * y⁻¹) = y * NormedSpace.exp 𝕂 x * y⁻¹
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedDivisionRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>y x : 𝔸<VAR>hy : y ≠ 0<GOAL>NormedSpace.exp 𝕂 (y⁻¹ * x * y) = y⁻¹ * NormedSpace.exp 𝕂 x * y
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedCommRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>x y : 𝔸<GOAL>NormedSpace.exp 𝕂 (x + y) = NormedSpace.exp 𝕂 x * NormedSpace.exp 𝕂 y
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>RCLike 𝕂<VAR>NormedCommRing 𝔸<VAR>NormedAlgebra 𝕂 𝔸<VAR>CompleteSpace 𝔸<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → 𝔸<GOAL>NormedSpace.exp 𝕂 (∑ i ∈ s, f i) = ∏ i ∈ s, NormedSpace.exp 𝕂 (f i)
<VAR>𝕂 : Type u_1<VAR>𝕂' : Type u_2<VAR>𝔸 : Type u_3<VAR>Field 𝕂<VAR>Field 𝕂'<VAR>Ring 𝔸<VAR>Algebra 𝕂 𝔸<VAR>Algebra 𝕂' 𝔸<VAR>TopologicalSpace 𝔸<VAR>TopologicalRing 𝔸<VAR>n : ℕ<VAR>x : 𝔸<GOAL>((NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x) = (NormedSpace.expSeries 𝕂' 𝔸 n) fun x_1 => x
<VAR>𝕂 : Type u_1<VAR>𝕂' : Type u_2<VAR>𝔸 : Type u_3<VAR>Field 𝕂<VAR>Field 𝕂'<VAR>Ring 𝔸<VAR>Algebra 𝕂 𝔸<VAR>Algebra 𝕂' 𝔸<VAR>TopologicalSpace 𝔸<VAR>TopologicalRing 𝔸<GOAL>NormedSpace.exp 𝕂 = NormedSpace.exp 𝕂'
<GOAL>NormedSpace.exp ℝ = NormedSpace.exp ℂ
<VAR>r : ℝ<GOAL>↑(NormedSpace.exp ℝ r) = NormedSpace.exp ℂ ↑r