coe_opLinearEquiv_addEquiv — Mathlib

English

The toAddEquiv of the map opLinearEquiv coincides with the additive equivalence opAddEquiv.

Русский

toAddEquiv линейного эквивалента opLinearEquiv совпадает с добавочным эквивалентом opAddEquiv.

LaTeX

$$coe_opLinearEquiv_addEquiv : ((opLinearEquiv R) : M ≃ₗ[R] Mᵐᵒᵖ) .toAddEquiv = opAddEquiv$$

Lean4

@[simp]
theorem coe_opLinearEquiv_addEquiv : ((opLinearEquiv R : M ≃ₗ[R] Mᵐᵒᵖ) : M ≃+ Mᵐᵒᵖ) = opAddEquiv :=
  rfl

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