Theorems · Definition · linear algebra

Module.Basis.addSubgroupOfClosure

{M : Type u_7} →
  {R : Type u_8} →
    [inst : Ring R] →
      [Nontrivial R] →
        [IsAddTorsionFree R] →
          [inst_3 : AddCommGroup M] →
            [inst_4 : Module R M] →
              (A : AddSubgroup M) →
                {ι : Type u_9} →
                  (b : Module.Basis ι R M) →
                    A = AddSubgroup.closure (Set.range ⇑b) → Module.Basis ι ℤ ↥(AddSubgroup.toIntSubmodule A)

Let A be a subgroup of an additive commutative group M that is also an R-module. Construct a basis of A as a ℤ-basis from an R-basis of E that generates A.

Defined in

Mathlib.LinearAlgebra.Basis.Submodule

Cited by

4 results in Mathlib

Foundations

Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingNontrivialIsAddTorsionFreeAddCommGroupModule