coe_toIntSubmodule — Mathlib

English

The set-theoretic image of an AddSubgroup under toIntSubmodule matches the corresponding Submodule image under the same correspondence.

Русский

Образ подмодуля AddSubgroup под toIntSubmodule совпадает с образом в Submodule при той же корреспонденции.

LaTeX

$$$(S : AddSubgroup M)^{\\toIntSubmodule} : Set M = S$$$

Lean4

@[simp]
theorem coe_toIntSubmodule (S : AddSubgroup M) : (S.toIntSubmodule : Set M) = S :=
  rfl

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