Theorems · Theorem · functional analysis
algebraMap_isometry
∀ (𝕜 : Type u_1) (𝕜' : Type u_2) [inst : NormedField 𝕜] [inst_1 : SeminormedRing 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] [NormOneClass 𝕜'], Isometry ⇑(algebraMap 𝕜 𝕜')
In a normed algebra, the inclusion of the base field in the extended field is an isometry.
- Defined in
- Mathlib.Analysis.Normed.Module.Basic
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 152 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
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
- Realproof · cited by 25,697
- RingHomstatement · cited by 10,189
- Norm.normproof · cited by 5,413
- Algebra.algebraMapstatement and proof · cited by 4,706
- Dist.distproof · cited by 1,539
- NormedAlgebrastatement and proof · cited by 1,165
- NormedFieldstatement and proof · cited by 1,084
- map_subproof · cited by 565
- SeminormedRingstatement and proof · cited by 446
- Isometrystatement · cited by 230
- dist_eq_normproof · cited by 182
Cited by4
Results whose statement or proof uses this declaration.
- SpectrumRestricts.spectralRadius_eqproof · cited by 3
- MeasureTheory.hasDerivAt_resolventTransformproof · cited by 1
- MeasureTheory.norm_resolvent_le_inv_infDist_supportproof · cited by 1
- MeasureTheory.analyticOn_resolventTransformproof · cited by 0