Theorems · Definition · commutative algebra
Submodule.LinearDisjoint.mulMap
{R : Type u} →
{S : Type v} →
[inst : CommSemiring R] →
[inst_1 : Semiring S] →
[inst_2 : Algebra R S] → {M N : Submodule R S} → M.LinearDisjoint N → TensorProduct R ↥M ↥N ≃ₗ[R] ↥(M * N)If M and N are linearly disjoint submodules, then there is the natural isomorphism
M ⊗[R] N ≃ₗ[R] M * N induced by multiplication in S.
- Defined in
- Mathlib.LinearAlgebra.LinearDisjoint
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommSemiringSemiringAlgebra
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- RingHom.idstatement · cited by 18,349
- Semiringstatement and proof · cited by 13,802
- Algebrastatement and proof · cited by 11,388
- CommSemiringstatement and proof · cited by 10,911
- Submodulestatement and proof · cited by 7,192
- LinearEquivstatement · cited by 3,317
- TensorProductstatement · cited by 2,545
- LinearMap.rangeproof · cited by 893
- LinearEquiv.transproof · cited by 298
- Submodule.LinearDisjointstatement and proof · cited by 54
- Submodule.mulMapproof · cited by 43
- LinearEquiv.ofEqproof · cited by 32
Cited by2
Results whose statement or proof uses this declaration.
- Ideal.eq_top_of_mk_tensor_eq_oneproof · cited by 0
- Submodule.LinearDisjoint.val_mulMap_tmulstatement · cited by 0