RingHom.laurentSeries_derivative_eq_of_kaehlerDifferential_D_eq_smul
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs.RingHomLaurentSeriesDerivative
universe u vLean source · statement
theorem _root_.RingHom.laurentSeries_derivative_eq_of_kaehlerDifferential_D_eq_smul {R : Type u}
{A : Type v} [CommRing R] [CommRing A] [Algebra R A]
(Λ : A →+* LaurentSeries R) (hΛC : ∀ r : R, Λ (algebraMap R A r) = HahnSeries.C r)
{t₀ : A} (ht₀ : Λ t₀ = HahnSeries.single 1 1) :
(∀ g c : A, KaehlerDifferential.D R A g = c • KaehlerDifferential.D R A t₀ →
LaurentSeries.derivative R (Λ g) = Λ c) ∧
(Nontrivial R → KaehlerDifferential.D R A t₀ ≠ 0)