Algebra.FormallySmooth.of_maximalIdeal_eq_span_of_perfectField
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Algebra_FormallySmooth_of_maximalIdeal_eq_span_of_perfectField
universe u v
open IsLocalRingLean source · statement
theorem _root_.Algebra.FormallySmooth.of_maximalIdeal_eq_span_of_perfectField
(K : Type u) [Field K] [PerfectField K] (𝒪 : Type v) [CommRing 𝒪] [IsLocalRing 𝒪] [IsDomain 𝒪]
[IsNoetherianRing 𝒪]
[Algebra K 𝒪] [Algebra.EssFiniteType K 𝒪]
(u : 𝒪) (hu0 : u ≠ 0) (hu : maximalIdeal 𝒪 = Ideal.span {u}) :
Algebra.FormallySmooth K 𝒪