Theorems · Theorem · commutative algebra
Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat_left
∀ {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 →
∀ [Nontrivial R] [Module.Flat R ↥M] (a b : ↥(M ⊓ N)), Commute ↑a ↑b → ¬LinearIndependent R ![a, b]If M and N are linearly disjoint, if M is flat, then any two commutative
elements of ↥(M ⊓ N) are not R-linearly independent (namely, their span is not R ^ 2).
- Defined in
- Mathlib.LinearAlgebra.LinearDisjoint
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites31
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- AddCommGroupproof · cited by 12,871
- Algebrastatement and proof · cited by 11,388
- Ringstatement and proof · cited by 7,463
- Submodulestatement and proof · cited by 7,192
- Finsuppproof · cited by 5,255
- Nontrivialstatement and proof · cited by 2,416
- sub_selfproof · cited by 996
- Finsupp.singleproof · cited by 943
- Matrix.vecConsstatement and proof · cited by 852
- Matrix.vecEmptystatement and proof · cited by 832
Cited by2
Results whose statement or proof uses this declaration.
- Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flatproof · cited by 2
- Submodule.LinearDisjoint.not_linearIndependent_pair_of_flat_leftproof · cited by 0