R : Type u_1
M : Type u_2
M₂ : Type ?u.1961009
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M
⊢ Ring.inverse ↑(↑(MulEquiv.symm (ContinuousLinearEquiv.unitsEquiv R M)) e) = inverse ↑e
R : Type u_1
M : Type u_2
M₂ : Type ?u.1961009
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M
⊢ Ring.inverse ↑e = inverse ↑e
suffices Ring.inverse ((ContinuousLinearEquiv.unitsEquiv _ _).symm e : M →L[R] M) = inverse ↑e by
  convert this
R : Type u_1
M : Type u_2
M₂ : Type ?u.1961009
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M
⊢ ↑(↑(MulEquiv.symm (ContinuousLinearEquiv.unitsEquiv R M)) e)⁻¹ = ↑(ContinuousLinearEquiv.symm e)
R : Type u_1
M : Type u_2
M₂ : Type ?u.1961009
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M
⊢ Ring.inverse ↑(↑(MulEquiv.symm (ContinuousLinearEquiv.unitsEquiv R M)) e) = inverse ↑e
simp
no goals
R : Type u_1
M : Type u_2
M₂ : Type ?u.1961009
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M
⊢ ↑(↑(MulEquiv.symm (ContinuousLinearEquiv.unitsEquiv R M)) e)⁻¹ = ↑(ContinuousLinearEquiv.symm e)
rfl
no goals
R : Type u_1
M : Type u_2
M₂ : Type ?u.1961009
inst✝⁷ : TopologicalSpace M
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalAddGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M ≃L[R] M
this : Ring.inverse ↑(↑(MulEquiv.symm (ContinuousLinearEquiv.unitsEquiv R M)) e) = inverse ↑e
⊢ Ring.inverse ↑e = inverse ↑e
convert this