restrictScalarsEquiv_symm_mk — Mathlib

English

The inverse of restrictScalarsEquiv acts trivially on canonical representatives mk x, i.e., (restrictScalarsEquiv S P).symm (mk x) = mk x.

Русский

Обратное отображение от restrictScalarsEquiv действует тривиально на канонических представителях mk x: (restrictScalarsEquiv S P).symm (mk x) = mk x.

LaTeX

$$$$ (\\text{restrictScalarsEquiv } S P)\\!^{-1} (\\mk x) = \\mk x. $$$$

Lean4

@[simp]
theorem restrictScalarsEquiv_symm_mk [Ring S] [SMul S R] [Module S M] [IsScalarTower S R M] (P : Submodule R M)
    (x : M) : (restrictScalarsEquiv S P).symm (mk x) = mk x :=
  rfl

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