Theorems · Definition · geometry

Submodule.toAffineSubspace

{k : Type u_1} →
  {V : Type u_2} →
    [inst : Ring k] → [inst_1 : AddCommGroup V] → [inst_2 : Module k V] → Submodule k V → AffineSubspace k V

Reinterprets p : Submodule k V as an AffineSubspace k V.

Defined in

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Cited by

6 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext

Assumes

RingAddCommGroupModule