ringInverse_equiv — Mathlib

English

Inverse of composition with an equivalence equals composition of inverses in swapped order.

Русский

Обратная к композиции с эквивалентом равна композиции обратных отображений в обратном порядке.

LaTeX

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

Lean4

@[simp]
theorem ringInverse_equiv (e : M ≃L[R] M) : Ring.inverse ↑e = inverse (e : M →L[R] M) :=
  by
  suffices Ring.inverse ((ContinuousLinearEquiv.unitsEquiv _ _).symm e : M →L[R] M) = inverse ↑e by convert this
  simp
  rfl

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