Theorems · Theorem · commutative algebra

Subalgebra.adjoin_eq_span_basis

∀ {F : Type u_1} (E : Type u_2) {K : Type u_3} [inst : CommSemiring E] [inst_1 : Semiring K] [inst_2 : SMul F E]
  [inst_3 : Algebra E K] [inst_4 : CommSemiring F] [inst_5 : Algebra F K] [IsScalarTower F E K] (L : Subalgebra F K)
  {ι : Type u_4} (bL : Module.Basis ι F ↥L),
  Subalgebra.toSubmodule (Algebra.adjoin E ↑L) = Submodule.span E (Set.range fun i => ↑(bL i))

If K / E / F is a ring extension tower, L is a subalgebra of K / F, then E[L] is generated by any basis of L / F as an E-module.

Defined in

Mathlib.RingTheory.Adjoin.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringSMulAlgebraCommSemiringAlgebraIsScalarTower