Some lemmas about linear maps

Stream: mathlib4

[Niels Voss]

I need the following lemmas (along with a few more I haven't proven yet) for #33731. Do these belong in mathlib?

import Mathlib

namespace LinearMap
open InnerProductSpace

variable {𝕜 : Type*} [RCLike 𝕜]
  {E : Type*} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E]
  {F : Type*} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F]
  (T : E →ₗ[𝕜] F)

theorem isSymmetric_self_comp_adjoint :
    (T ∘ₗ adjoint T).IsSymmetric := T.isPositive_self_comp_adjoint.isSymmetric

-- LinearMap.isSymmetric_adjoint_mul_self but domain and range can be different
theorem isSymmetric_adjoint_comp_self
  : (adjoint T ∘ₗ T).IsSymmetric := T.isPositive_adjoint_comp_self.isSymmetric

theorem eigenvalues_adjoint_comp_self_nonneg
  {n : ℕ} (hn : Module.finrank 𝕜 E = n) (i : Fin n)
  : 0 ≤ (LinearMap.isSymmetric_adjoint_comp_self T).eigenvalues hn i := by
  apply LinearMap.IsPositive.nonneg_eigenvalues
  exact T.isPositive_adjoint_comp_self

/--
7.64(b) in [axler2024].
-/
lemma ker_adjoint_comp_self : ker (adjoint T ∘ₗ T) = ker T := by
  apply le_antisymm
  · intro v hv
    have := calc
      ‖T v‖ ^ 2 = ⟪T v, T v⟫_𝕜 := (inner_self_eq_norm_sq_to_K (T v)).symm
      _ = ⟪(adjoint T ∘ₗ T) v, v⟫_𝕜 := (adjoint_inner_left T v (T v)).symm
      _ = ⟪0, v⟫_𝕜 := by rw [hv]
      _ = 0 := inner_zero_left v
    simp_all
  · intro v hv
    simp_all

lemma injective_adjoint_comp_self_iff
  : Function.Injective (adjoint T ∘ₗ T) ↔ Function.Injective T := by
  repeat rw [←LinearMap.ker_eq_bot]
  rw [ker_adjoint_comp_self]