Theorems · Theorem · functional analysis
ContinuousLinearMap.IsIdempotentElem.toLinearMap
∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
[inst_3 : Module R M] {f : M →L[R] M}, IsIdempotentElem f → IsIdempotentElem ↑fAlias of the reverse direction of ContinuousLinearMap.isIdempotentElem_toLinearMap_iff.
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 27 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- Modulestatement and proof · cited by 20,661
- RingHom.idstatement and proof · cited by 18,349
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- LinearMapstatement · cited by 10,215
- ContinuousLinearMapstatement and proof · cited by 5,352
- ContinuousLinearMap.toLinearMapstatement · cited by 528
- IsIdempotentElemstatement · cited by 217
- ContinuousLinearMap.isIdempotentElem_toLinearMap_iffproof · cited by 1
Cited by13
Results whose statement or proof uses this declaration.
- ContinuousLinearMap.IsIdempotentElem.isTopComplproof · cited by 5
- Submodule.isSymmetricProjection_starProjectionproof · cited by 3
- ContinuousLinearMap.IsIdempotentElem.range_mem_invtSubmodule_iffproof · cited by 3
- ContinuousLinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iffproof · cited by 3
- ContinuousLinearMap.IsIdempotentElem.isPositive_iff_isSelfAdjointproof · cited by 2
- ContinuousLinearMap.IsIdempotentElem.commute_iffproof · cited by 1
- ContinuousLinearMap.IsIdempotentElem.eq_projectionLproof · cited by 1
- ContinuousLinearMap.IsIdempotentElem.ext_iffproof · cited by 1
- InnerProductSpace.isSymmetricProjection_rankOne_selfproof · cited by 1
- Submodule.ker_starProjectionproof · cited by 0
- ContinuousLinearMap.IsIdempotentElem.TFAEproof · cited by 0
- ContinuousLinearMap.IsIdempotentElem.commute_iff_of_isUnitproof · cited by 0