inverse_equiv_comp — Mathlib

English

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

Русский

Обратная равна $f^{-1} \circ e^{-1}$ для композиции с эквивалентом.

LaTeX

$$$(e \circ_L f).inverse = f.inverse \circ_L (e.symm : M_3 \to_L[R] M_2)$$$

Lean4

@[simp]
theorem inverse_equiv_comp {e : M₂ ≃L[R] M₃} {f : M →L[R] M₂} :
    (e ∘L f).inverse = f.inverse ∘L (e.symm : M₃ →L[R] M₂) :=
  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, zero_comp]

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