Theorems · Theorem · commutative algebra
TensorProduct.span_tmul_eq_top
∀ (R : Type u_1) [inst : CommSemiring R] (M : Type u_7) (N : Type u_8) [inst_1 : AddCommMonoid M]
[inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N],
Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} = ⊤The simple (aka pure) elements span the tensor product.
- Defined in
- Mathlib.LinearAlgebra.TensorProduct.Defs
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 56 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- AddCommMonoidstatement and proof · cited by 12,281
- CommSemiringstatement and proof · cited by 10,911
- Top.topstatement · cited by 9,680
- Submodulestatement · cited by 7,192
- Set.ofPredstatement and proof · cited by 6,101
- TensorProductstatement and proof · cited by 2,545
- Submodule.spanstatement and proof · cited by 1,504
- TensorProduct.tmulstatement and proof · cited by 1,182
- Submodule.subset_spanproof · cited by 234
- Submodule.extproof · cited by 204
- TensorProduct.induction_onproof · cited by 81
Cited by8
Results whose statement or proof uses this declaration.
- Submodule.baseChange_topproof · cited by 5
- Submodule.baseChange_eq_spanproof · cited by 4
- TensorProduct.mk_surjectiveproof · cited by 4
- Algebra.QuasiFinite.of_restrictScalarsproof · cited by 3
- TensorProduct.flip_mk_surjectiveproof · cited by 1
- Algebra.TensorProduct.adjoin_tmul_eq_topproof · cited by 1
- Module.FaithfullyFlat.range_le_ker_of_exact_rTensorproof · cited by 1
- TensorProduct.map₂_mk_top_top_eq_topproof · cited by 0