Theorems · Theorem · functional analysis
RingHomIsometric.nnnorm_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
- 3 results in Mathlib
- Foundations
- Depth 114 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
- NNRealstatement · cited by 4,310
- NNNorm.nnnormstatement · cited by 952
- SeminormedRingstatement and proof · cited by 446
- RingHomIsometricstatement and proof · cited by 282
- NNReal.eqproof · cited by 201
- RingHomIsometric.norm_mapproof · cited by 9
Cited by3
Results whose statement or proof uses this declaration.
- ContinuousLinearMap.exists_lt_apply_of_lt_opNNNormproof · cited by 3
- ContinuousLinearMap.exists_nnnorm_eq_one_lt_apply_of_lt_opNNNormproof · cited by 1
- RingHomIsometric.enorm_mapproof · cited by 0