Theorems · Theorem · functional analysis
NormedSpace.exp_def
∀ {𝔸 : Type u_3} [inst : Ring 𝔸] [inst_1 : TopologicalSpace 𝔸] [inst_2 : IsTopologicalRing 𝔸] (x : 𝔸),
NormedSpace.exp x = if h : Nonempty (Algebra ℚ 𝔸) then (NormedSpace.expSeries ℚ 𝔸).sum x else 1- Cited by
- 3 results in Mathlib
- Foundations
- Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- Algebrastatement and proof · cited by 11,388
- Ringstatement and proof · cited by 7,463
- IsTopologicalRingstatement and proof · cited by 402
- Nonempty.somestatement · cited by 340
- NormedSpace.expstatement · cited by 157
- NormedSpace.expSeriesstatement and proof · cited by 68
- FormalMultilinearSeries.sumstatement and proof · cited by 34
Cited by3
Results whose statement or proof uses this declaration.
- NormedSpace.exp_zeroproof · cited by 8
- NormedSpace.exp_eq_expSeries_sumproof · cited by 8
- NormedSpace.exp_of_isEmpty_algebra_ratproof · cited by 3