Theorems · Theorem · commutative algebra

Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat

∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {M N : Submodule R S},
  M.LinearDisjoint N →
    Module.Flat R ↥M ∨ Module.Flat R ↥N → (∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n) → Module.rank R ↥(M ⊓ N) ≤ 1

If M and N are linearly disjoint, if one of M and N is flat, if any two elements of ↥(M ⊓ N) are commutative, then the rank of ↥(M ⊓ N) is at most one.

Defined in

Mathlib.LinearAlgebra.LinearDisjoint

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommRingRingAlgebra