toAffineSubspace — Mathlib

English

Every submodule can be viewed as an affine subspace with the same carrier.

Русский

Каждый подмодуль можно рассматривать как аффинное подпространство с тем же носителем.

LaTeX

$$$\\mathrm{toAffineSubspace}(p) \\text{ имеет carrier } p$$$

Lean4

/-- Reinterpret `p : Submodule k V` as an `AffineSubspace k V`. -/
def toAffineSubspace (p : Submodule k V) : AffineSubspace k V
    where
  carrier := p
  smul_vsub_vadd_mem _ _ _ _ h₁ h₂ h₃ := p.add_mem (p.smul_mem _ (p.sub_mem h₁ h₂)) h₃

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