Algebra.FormallySmooth.quotient_span_singleton_of_existsUnique_eq_smul_D
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallySmooth_quotient_span_singleton_of_existsUnique_eq_smul_D
open PolynomialLean source · statement
theorem _root_.Algebra.FormallySmooth.quotient_span_singleton_of_existsUnique_eq_smul_D
{A : Type} [CommRing A] {S : Type} [CommRing S] [Algebra A S] [Algebra.FormallySmooth A S]
(t : S) (hdt : ∀ ω : Ω[S⁄A], ∃! s : S, ω = s • KaehlerDifferential.D A S t) :
Algebra.FormallySmooth A (S ⧸ Ideal.span ({t} : Set S))