Theorems · Theorem · linear algebra
Submodule.coe_span_eq_self
∀ {R : Type u_1} {M : Type u_4} {S : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
[inst_3 : SetLike S M] [AddSubmonoidClass S M] [SMulMemClass S R M] (s : S), ↑(Submodule.span R ↑s) = ↑sA version of Submodule.span_eq for subobjects closed under addition and scalar multiplication
and containing zero. In general, this should not be used directly, but can be used to quickly
generate proofs for specific types of subobjects.
- Defined in
- Mathlib.LinearAlgebra.Span.Defs
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Modulestatement and proof · cited by 20,661
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- SetLike.coestatement and proof · cited by 8,199
- Submodulestatement and proof · cited by 7,192
- le_antisymmproof · cited by 2,068
- le_rflproof · cited by 1,558
- Submodule.spanstatement · cited by 1,504
- SetLikestatement and proof · cited by 1,084
- AddSubmonoidClassstatement and proof · cited by 346
- Submodule.subset_spanproof · cited by 234
Cited by2
Results whose statement or proof uses this declaration.
- NonUnitalStarAlgebra.span_eq_toSubmoduleproof · cited by 1
- NonUnitalAlgebra.span_eq_toSubmoduleproof · cited by 0