Structures Β· Analysis
NormedAlgebra
A normed algebra π' over π is normed module that is also an algebra.
See the implementation notes for Algebra for a discussion about non-unital algebras. Following
the strategy there, a non-unital normed algebra can be written as:
``lean
variable [NormedField π] [NonUnitalSeminormedRing π']
variable [NormedSpace π π'] [SMulCommClass π π' π'] [IsScalarTower π π' π']
``
- Defined in
- Mathlib.Analysis.Normed.Module.Basic
- Shape
- 2 explicit arguments Β· adds norm_smul_le
Extends1
Extended by2
Concrete types that are instances4
- Real
- Rat
- Complex
- Padic
How is a type an instance?
Loading the hierarchy indexβ¦
Assumed by1,253
- logDeriv
- ContinuousLinearMap.lsmul
- HasDerivAt.comp
- SchwartzMap.smulLeftCLM
- norm_algebraMap'
- NormedSpace.restrictScalars
- intervalIntegral.integral_const_mul
- NormedSpace.expSeries_radius_eq_top
- HasDerivAt.const_mul
- HasDerivAt.comp_hasFDerivWithinAt
- HasDerivAt.comp_hasDerivWithinAt
- HasStrictDerivAt.comp
- HasDerivAt.mul
- HasDerivAt.comp_hasFDerivAt
- selfAdjoint.expUnitary
- HasStrictDerivAt.comp_hasStrictFDerivAt
- HasDerivAt.div_const
- AnalyticAt.smul
- CFC.log
- deriv_fun_mul
- MeromorphicAt.zpow
- DifferentiableAt.mul
- MeromorphicAt.smul
- AnalyticAt.inv
- formalMultilinearSeries_geometric
- SchwartzMap.smulLeftCLM_apply_apply
- DifferentiableAt.const_mul
- Complex.contDiff_exp
- HasDerivAt.scomp
- spectrum.norm_le_norm_of_mem
- ContinuousLinearMap.bilinearRestrictScalars
- meromorphicOrderAt_smul
- AnalyticAt.fun_smul
- HasFDerivAt.restrictScalars
- DifferentiableAt.div_const
- AnalyticAt.pow
- MeromorphicAt.inv
- deriv_fun_pow
- alternatingGeometricSeries
- Differentiable.mul
- deriv_comp
- DifferentiableAt.inv
- AnalyticAt.zpow
- selfAdjoint.expUnitary_coe
- HasDerivAt.pow
- NormedSpace.exp_add_of_commute
- HasDerivAt.mul_const
- spectrum.nonempty
- ContDiff.mul
- Differentiable.const_mul