isInvertible_comp_equiv — Mathlib

English

If e is a continuous linear equivalence, then (f ∘ e).IsInvertible iff f.IsInvertible.

Русский

Если $e$ — непрерывное линейное эквивалентное отображение, то $(f \circ e)$ обратимо тогда и только тогда, когда $f$ обратимо.

LaTeX

$$$(f \circ_L e.toContinuousLinearMap).IsInvertible \iff f.IsInvertible$$$

Lean4

@[simp]
theorem isInvertible_comp_equiv {e : M₃ ≃L[R] M} {f : M →L[R] M₂} :
    (f ∘L (e : M₃ →L[R] M)).IsInvertible ↔ f.IsInvertible :=
  by
  constructor
  · rintro ⟨A, hA⟩
    have : f = (f ∘L (e : M₃ →L[R] M)) ∘L e.symm := by ext; simp
    rw [this, ← hA]
    simp
  · rintro ⟨M, rfl⟩
    simp

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