Algebra.Smooth.isReduced_of_isReduced_of_isNoetherianRing
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Algebra_Smooth_isReduced_of_isReduced_of_isNoetherianRing
universe u
open CategoryTheory AlgebraicGeometryLean source · statement
theorem _root_.Algebra.Smooth.isReduced_of_isReduced_of_isNoetherianRing
(R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Algebra.Smooth R S]
[IsReduced R] [IsNoetherianRing R] : IsReduced S