Subalgebra.fg_restrictScalars_and_le_of_fg
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Subalgebra_fg_restrictScalars_and_le_of_fg
universe uLean source · statement
theorem _root_.Subalgebra.fg_restrictScalars_and_le_of_fg
{A₀ A : Type u} [CommRing A₀] [CommRing A] [Algebra A₀ A]
(T : Subalgebra A₀ A) (hT : T.FG) (T' : Subalgebra ↥T A) (hT' : T'.FG) :
(T'.restrictScalars A₀).FG ∧ (T : Set A) ⊆ (T'.restrictScalars A₀ : Set A)