Theorems · Theorem · linear algebra

Module.Basis.addSubgroupOfClosure_apply

∀ {M : Type u_7} {R : Type u_8} [inst : Ring R] [inst_1 : Nontrivial R] [inst_2 : IsAddTorsionFree R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (A : AddSubgroup M) {ι : Type u_9} (b : Module.Basis ι R M)
  (h : A = AddSubgroup.closure (Set.range ⇑b)) (i : ι), ↑((Module.Basis.addSubgroupOfClosure A b h) i) = b i

Defined in

Mathlib.LinearAlgebra.Basis.Submodule

Cited by

2 results in Mathlib

Foundations

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

Assumes

RingNontrivialIsAddTorsionFreeAddCommGroupModule