Mathlib Map

Theorems · Theorem · functional analysis

NormedSpace.exp_smul

∀ {𝔸 : Type u_1} [inst : NormedRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] {G : Type u_3} [inst_3 : Monoid G]
  [inst_4 : MulSemiringAction G 𝔸] [ContinuousConstSMul G 𝔸] (g : G) (x : 𝔸),
  NormedSpace.exp (g • x) = g • NormedSpace.exp x
Defined in
Mathlib.Analysis.Normed.Algebra.Exponential
Cited by
1 results in Mathlib
Foundations
Depth 179 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
NormedRingNormedAlgebraCompleteSpaceMonoidMulSemiringActionContinuousConstSMul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

NormedSpace.exp_units_conj · cited by 3NormedSpace.exp_units_conjMonoid · cited by 3887MonoidCompleteSpace · cited by 2532CompleteSpaceNormedAlgebra · cited by 1165NormedAlgebraNormedRing · cited by 924NormedRingContinuousConstSMul · cited by 832ContinuousConstSMulMulSemiringAction · cited by 423MulSemiringActionNormedSpace.exp · cited by 157NormedSpace.expContinuousConstSMul.continuous_const_smul · cited by 25ContinuousConstSMul.conti…MulSemiringAction.toRingHom · cited by 23MulSemiringAction.toRingH…NormedSpace.map_exp · cited by 7NormedSpace.map_expNormedSpace.exp_smulCITED BYCITES

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.