mapEvalEquiv_symm_apply — Mathlib

English

The inverse of mapEvalEquiv acts by comapping with Dual.eval: (mapEvalEquiv R M).symm W'' = W''.comap(Dual.eval R M).

Русский

Обратная карта mapEvalEquiv действует через comap с Dual.eval: (mapEvalEquiv R M).symm W'' = W''.comap(Dual.eval R M).

LaTeX

$$ (mapEvalEquiv(R,M)).symm W'' = W''.comap(Dual.eval(R,M)).$$

Lean4

@[simp]
theorem mapEvalEquiv_symm_apply (W'' : Submodule R (Dual R (Dual R M))) :
    (mapEvalEquiv R M).symm W'' = W''.comap (Dual.eval R M) :=
  rfl

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