ker_starProjection — Mathlib

English

The kernel of the starProjection equals the orthogonal complement: ker K.starProjection = K^⊥.

Русский

Ядро starProjection равно ортогональному дополнению: ker K.starProjection = K^⊥.

LaTeX

$$ker(K.starProjection) = K^{\perp}.$$

Lean4

@[simp]
theorem ker_starProjection (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] : LinearMap.ker U.starProjection = Uᗮ := by
  rw [(isIdempotentElem_starProjection U).ker_eq_range, ← starProjection_orthogonal', range_starProjection]

Похожие утверждения