Theorems · Inductive type · operator theory

LinearMap.IsSymmetricProjection

{𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] → [inst_1 : SeminormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → (E →ₗ[𝕜] E) → Prop

A symmetric projection is a symmetric idempotent.

Defined in: Mathlib.Analysis.InnerProductSpace.Symmetric
Cited by: 21 results in Mathlib
Foundations: Depth 46 from the axioms · uses propext, Quot.sound
Assumes: RCLike SeminormedAddCommGroup InnerProductSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

RingHom.idstatement · cited by 18,349
LinearMapstatement · cited by 10,215
InnerProductSpacestatement · cited by 3,523
RCLikestatement · cited by 2,829
SeminormedAddCommGroupstatement · cited by 2,671

Cited by23

Results whose statement or proof uses this declaration.

LinearMap.IsSymmetricProjection.isIdempotentElemstatement and proof · cited by 6
LinearMap.IsSymmetricProjection.isSymmetricstatement and proof · cited by 6
ContinuousLinearMap.isStarProjection_iff_isSymmetricProjectionstatement · cited by 3
Submodule.isSymmetricProjection_starProjectionstatement · cited by 3
LinearMap.IsSymmetricProjection.ext_iffstatement and proof · cited by 2
Submodule.isSymmetricProjection_projection_iffstatement · cited by 2
ContinuousLinearMap.IsStarProjection.isSymmetricProjectionstatement · cited by 1
ContinuousLinearMap.LinearMap.IsSymmetricProjection.isStarProjectionstatement · cited by 1
LinearMap.isSymmetricProjection_iff_eq_coe_starProjectionstatement and proof · cited by 1
LinearMap.isSymmetricProjection_iff_eq_coe_starProjection_rangestatement and proof · cited by 1
LinearMap.IsSymmetricProjection.casesOnstatement and proof · cited by 1
InnerProductSpace.isSymmetricProjection_rankOne_selfstatement · cited by 1