Structures · Analysis
RingHomIsometric
This class states that a ring homomorphism is isometric. This is a sufficient assumption for a continuous semilinear map to be bounded and this is the main use for this typeclass.
- Defined in
- Mathlib.Analysis.Normed.Ring.Basic
- Shape
- One type argument · adds norm_map
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by326
- ContinuousLinearMap.flip
- ContinuousLinearMap.le_opNorm
- Seminorm.comp
- ContinuousLinearMap.integrable_comp
- ContinuousLinearMap.le_of_opNorm_le
- ContinuousLinearMap.compLp
- ContinuousLinearMap.lipschitz
- ContinuousLinearMap.opNorm_comp_le
- ContinuousLinearMap.le_opNorm₂
- ContinuousLinearMap.precomp
- LinearIsometry.norm_toContinuousLinearMap
- ContinuousLinearMap.bilinearComp
- ContinuousLinearMap.le_opENorm
- ContinuousLinearMap.compLpL
- ContinuousLinearMap.coeFn_compLp
- RingHomIsometric.norm_map
- SeminormFamily.comp
- ContinuousLinearEquiv.antilipschitz
- LinearMap.mkContinuous₂_norm_le
- ContinuousLinearMap.opNorm_flip
- ContinuousLinearEquiv.ofBijective
- Seminorm.IsBounded
- ContinuousLinearMap.isOpenMap
- ContinuousLinearMap.le_opNNNorm
- ContinuousLinearMap.equivRange
- ContinuousLinearEquiv.arrowCongrSL
- ContinuousLinearMap.compSL
- ContinuousLinearEquiv.lipschitz
- Bundle.Trivialization.continuousLinearMap
- Bornology.IsVonNBounded.image
- ContinuousLinearMap.le_opNorm_of_le
- LinearMap.mkContinuous₂
- ContinuousLinearMap.opNNNorm_le_bound
- LinearMap.withSeminorms_induced
- ContinuousLinearMap.apply'
- ContinuousLinearMap.bilinearComp.congr_simp
- ContinuousLinearMap.opNorm_le_of_shell
- MeasureTheory.Integrable.apply_continuousLinearMap
- ContinuousLinearMap.opNorm_le_iff
- ContinuousLinearMap.flip_flip
- ContinuousLinearMap.unit_le_opNorm
- ContinuousLinearMap.compLpₗ
- ContinuousLinearMap.le_of_opNorm_le_of_le
- Topology.IsInducing.withSeminorms
- ContinuousLinearEquiv.integrable_comp_iff
- RingHom.isometry
- WithSeminorms.continuous_normedSpace_rng
- WithSeminorms.continuous_of_isBounded
- ContinuousLinearMap.le_of_opNorm₂_le_of_le
- ContinuousLinearMap.isBigO_comp
Ancestors0
No ancestors.