toNatSubmodule — Mathlib

English

The natural-submonoid view of an additive submonoid respects the coe to submodule under the Nat-submodule correspondence.

Русский

Единый взгляд на аддитивный подмономод как на векторное подмодульное множество сохраняется при преобразовании между AddSubmonoid и Submodule ℕ через когерентность.

LaTeX

$$$(S.toNatSubmonoid : Set M) = S$$$

Lean4

/-- An additive submonoid is equivalent to a ℕ-submodule. -/
def toNatSubmodule : AddSubmonoid M ≃o Submodule ℕ M
    where
  toFun S := { S with smul_mem' := fun r s hs ↦ show r • s ∈ S from nsmul_mem hs _ }
  invFun := Submodule.toAddSubmonoid
  map_rel_iff' := Iff.rfl

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