Theorems · Theorem · functional analysis
NormedSpace.map_exp
∀ {𝔸 : Type u_1} {𝔹 : Type u_2} [inst : NormedRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] [inst_3 : NormedRing 𝔹]
[Algebra ℚ 𝔹] {F : Type u_3} [inst_5 : FunLike F 𝔸 𝔹] [RingHomClass F 𝔸 𝔹] (f : F),
Continuous ⇑f → ∀ (x : 𝔸), f (NormedSpace.exp x) = NormedSpace.exp (f x)Any continuous ring homomorphism commutes with NormedSpace.exp.
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 178 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Algebrastatement and proof · cited by 11,388
- Continuousstatement and proof · cited by 2,592
- FunLikestatement and proof · cited by 2,560
- CompleteSpacestatement and proof · cited by 2,532
- NormedAlgebrastatement and proof · cited by 1,165
- NormedRingstatement and proof · cited by 924
- RingHomClassstatement and proof · cited by 193
- NormedSpace.expstatement · cited by 157
- edist_lt_topproof · cited by 32
- NormedSpace.expSeries_radius_eq_topproof · cited by 27
- NormedSpace.map_exp_of_mem_ballproof · cited by 2
Cited by7
Results whose statement or proof uses this declaration.
- CFC.exp_eq_normedSpace_expproof · cited by 5
- NormedSpace.exp_smulproof · cited by 1
- Pi.coe_expproof · cited by 1
- Quaternion.exp_coeproof · cited by 1
- NormedSpace.ofReal_exp_ℝ_ℝproof · cited by 0
- Prod.fst_expproof · cited by 0
- Prod.snd_expproof · cited by 0