inverse_comp_equiv — Mathlib

English

The inverse of (f ∘ e) equals e.symm ∘ f.inverse.

Русский

Обратная к $f \circ e$ равна $e^{-1} \circ f^{-1}$.

LaTeX

$$$(f \circ_L e).inverse = e.symm.toContinuousLinearMap \circ_L f.inverse$$$

Lean4

@[simp]
theorem inverse_comp_equiv {e : M₃ ≃L[R] M} {f : M →L[R] M₂} : (f ∘L e).inverse = (e.symm : M →L[R] M₃) ∘L f.inverse :=
  by
  by_cases hf : f.IsInvertible
  · rcases hf with ⟨A, rfl⟩
    simp only [ContinuousLinearEquiv.comp_coe, inverse_equiv, ContinuousLinearEquiv.coe_inj]
    rfl
  · rw [inverse_of_not_isInvertible (by simp [hf]), inverse_of_not_isInvertible hf, comp_zero]

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