toAddSubmonoid_toNatSubmodule — Mathlib

English

The natural-submonoid to submodule correspondence commutes with the toAddSubmonoid operation.

Русский

Корреспонденция между естественным подмодулем и подмодулем сохраняется при операции toAddSubmonoid.

LaTeX

$$$\\text{toAddSubmonoid} \\circ \\text{toNatSubmodule} = \\text{toNatSubmodule} \\circ \\text{toAddSubmonoid}$$$

Lean4

@[simp]
theorem toAddSubmonoid_toNatSubmodule (S : Submodule ℕ M) : S.toAddSubmonoid.toNatSubmodule = S :=
  AddSubmonoid.toNatSubmodule.apply_symm_apply S

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