inverse_comp_apply_of_right — Mathlib

English

For a linear equivalence e, the inverse of (f ∘ e) equals e⁻¹ ∘ f⁻¹.

Русский

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

LaTeX

$$ (f ∘L e).inverse = e.symm.toContinuousLinearMap ∘L f.inverse $$

Lean4

theorem inverse_comp_apply_of_right {g : M₂ →L[R] M₃} {f : M →L[R] M₂} {v : M₃} (hf : f.IsInvertible) :
    (g ∘L f).inverse v = f.inverse (g.inverse v) := by
  simp only [hf.inverse_comp_of_right, coe_comp', Function.comp_apply]

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