Theorems · Theorem · functional analysis
RingHomIsometric.enorm_map
∀ {R₁ : Type u_5} {R₂ : Type u_6} [inst : SeminormedRing R₁] [inst_1 : SeminormedRing R₂] (σ : R₁ →+* R₂)
[RingHomIsometric σ] (x : R₁), ‖σ x‖ₑ = ‖x‖ₑ- Defined in
- Mathlib.Analysis.Normed.Ring.Basic
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 115 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.
- DFunLike.coestatement · cited by 62,936
- RingHomstatement and proof · cited by 10,189
- ENNRealstatement · cited by 9,879
- ENNReal.ofNNRealproof · cited by 1,279
- ENorm.enormstatement · cited by 715
- SeminormedRingstatement and proof · cited by 446
- RingHomIsometricstatement and proof · cited by 282
- RingHomIsometric.nnnorm_mapproof · cited by 3
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.