Algebra.IsStandardSmooth.exists_isStandardSmoothOfRelativeDimension_of_field
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_IsStandardSmooth_exists_isStandardSmoothOfRelativeDimension_of_fieldLean source · statement
theorem _root_.Algebra.IsStandardSmooth.exists_isStandardSmoothOfRelativeDimension_of_field
{k : Type*} [Field k] {B : Type*} [CommRing B] [Algebra k B]
[Algebra.IsStandardSmooth k B] :
∃ n, Algebra.IsStandardSmoothOfRelativeDimension n k B