Theorems · Theorem · commutative algebra

exists_subalgebra_of_fg

∀ (A : Type w) (B : Type u₁) (C : Type u_1) [inst : CommSemiring A] [inst_1 : CommSemiring B] [inst_2 : Semiring C]
  [inst_3 : Algebra A B] [inst_4 : Algebra B C] [inst_5 : Algebra A C] [IsScalarTower A B C],
  ⊤.FG → ⊤.FG → ∃ B₀, B₀.FG ∧ ⊤.FG

Defined in

Mathlib.RingTheory.Adjoin.Tower

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringSemiringAlgebraAlgebraAlgebraIsScalarTower