lmulEquiv_eq_lidOfCompatibleSMul — Mathlib

English

For CompatibleSMul, the left multiplication isomorphism lmulEquiv is equal to the canonical lidOfCompatibleSMul map, i.e., they are the same algebra isomorphism S ⊗_R S ≅_S S.

Русский

При согласованных действиях, изоморфизм левого умножения совпадает с каноническим сопоставлением lidOfCompatibleSMul.

LaTeX

$$$ \mathrm{lmulEquiv} = \mathrm{lidOfCompatibleSMul} \; (\text{as algebra isomorphisms}) $$$

Lean4

theorem lmulEquiv_eq_lidOfCompatibleSMul [CompatibleSMul R S S S] : lmulEquiv R S = lidOfCompatibleSMul R S S :=
  AlgEquiv.coe_algHom_injective <| by ext; rfl

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