Theorems · Theorem · commutative algebra
Subalgebra.LinearDisjoint.of_linearDisjoint_finite_right
∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (A B : Subalgebra R S)
[Algebra.IsIntegral R ↥B], (∀ B' ≤ B, ∀ [Module.Finite R ↥B'], A.LinearDisjoint B') → A.LinearDisjoint BIf B/R is integral, such that A and B' are linearly disjoint for all subalgebras B'
of B which are finitely generated R-modules, then A and B are linearly disjoint.
- Defined in
- Mathlib.RingTheory.LinearDisjoint
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 124 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- Subalgebrastatement and proof · cited by 1,353
- Module.Finitestatement and proof · cited by 1,032
- Algebra.IsIntegralstatement and proof · cited by 224
- Subalgebra.LinearDisjointstatement and proof · cited by 75
- Subalgebra.LinearDisjoint.symmproof · cited by 7
- Subalgebra.LinearDisjoint.of_linearDisjoint_finite_leftproof · cited by 2
Cited by1
Results whose statement or proof uses this declaration.
- Subalgebra.LinearDisjoint.of_linearDisjoint_finiteproof · cited by 0