Theorems · Inductive type · commutative algebra

Submodule.LinearDisjoint

{R : Type u} →
  {S : Type v} →
    [inst : CommSemiring R] → [inst_1 : Semiring S] → [inst_2 : Algebra R S] → Submodule R S → Submodule R S → Prop

Two submodules M and N in an algebra S over R are linearly disjoint if the natural map M ⊗[R] N →ₗ[R] S induced by multiplication in S is injective.

Defined in

Mathlib.LinearAlgebra.LinearDisjoint

Cited by

54 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringSemiringAlgebra