Theorems · Definition · functional analysis
LinearIsometryEquiv.refl
(R : Type u_1) → (E : Type u_5) → [inst : Semiring R] → [inst_1 : SeminormedAddCommGroup E] → [inst_2 : Module R E] → E ≃ₗᵢ[R] E
Identity map as a LinearIsometryEquiv.
- Cited by
- 23 results in Mathlib
- Foundations
- Depth 28 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- RingHom.idstatement · cited by 18,349
- Semiringstatement and proof · cited by 13,802
- SeminormedAddCommGroupstatement and proof · cited by 2,671
- LinearIsometryEquivstatement · cited by 748
- LinearEquiv.reflproof · cited by 143
Cited by26
Results whose statement or proof uses this declaration.
- EuclideanSpace.basisFunproof · cited by 26
- LinearIsometryEquiv.lTensorproof · cited by 5
- LinearIsometryEquiv.rTensorproof · cited by 5
- Orientation.rotation_zerostatement · cited by 3
- LinearIsometryEquiv.trans_reflstatement · cited by 2
- LinearIsometryEquiv.refl_transstatement · cited by 2
- linear_isometry_complexproof · cited by 1
- linear_isometry_complex_auxstatement and proof · cited by 1
- LinearIsometryEquiv.mul_reflstatement · cited by 1
- Submodule.reflection_trans_reflectionstatement · cited by 1
- LinearIsometryEquiv.self_trans_symmstatement · cited by 0
- TensorProduct.congrIsometry_refl_reflstatement and proof · cited by 0