Module

KaehlerDifferential_exists_unique_smul_D_of_transcendental.lean

Nyll.AlgebraicCurves.Differentials.Kaehler.KaehlerDifferential_exists_unique_smul_D_of_transcendental

2 declarations indexed from sourceView source ↗

Module documentation

Kaehler Differential exists unique smul D of transcendental

Imports6

Nyll.AlgebraicCurves.Differentials.Kaehler.KaehlerDifferential_span_D_eq_top_of_transcendental
Nyll.AlgebraicCurves.Differentials.Kaehler.KaehlerDifferential_D_ne_zero_of_transcendental
Mathlib.RingTheory.Kaehler.Basic
Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Mathlib.FieldTheory.Separable
Mathlib.RingTheory.Algebraic.Defs

Imported by6

theorem

exists_unique_smul_D_of_transcendental

L34 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.KaehlerDifferential_exists_unique_smul_D_of_transcendental.KaehlerDifferential.exists_unique_smul_D_of_transcendental

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs
namespace KaehlerDifferential_exists_unique_smul_D_of_transcendental
open scoped _root_.KaehlerDifferential in

Lean source · statement

theorem KaehlerDifferential.exists_unique_smul_D_of_transcendental (K : Type*) [Field K] {F
  : Type*} [Field F] [Algebra K F] (x : F) (hx : Transcendental K x) [Algebra.IsSeparable
  (IntermediateField.adjoin K ({x} : Set F)) F] (ω : KaehlerDifferential K F) : ∃! c : F, ω = c •
  KaehlerDifferential.D K F x

theorem

exists_unique_smul_D_of_transcendental

L50 ↗

KaehlerDifferential.exists_unique_smul_D_of_transcendental

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs
namespace KaehlerDifferential_exists_unique_smul_D_of_transcendental
open KaehlerDifferential_exists_unique_smul_D_of_transcendental.KaehlerDifferential
  renaming exists_unique_smul_D_of_transcendental → uniqueSmulProof in

Lean source · statement

theorem _root_.KaehlerDifferential.exists_unique_smul_D_of_transcendental (K : Type*) [Field K] {F
  : Type*} [Field F] [Algebra K F] (x : F) (hx : Transcendental K x) [Algebra.IsSeparable
  (IntermediateField.adjoin K ({x} : Set F)) F] (ω : KaehlerDifferential K F) : ∃! c : F, ω = c •
  KaehlerDifferential.D K F x

Module documentation

Kaehler Differential exists unique smul D of transcendental

Declarations

exists_unique_smul_D_of_transcendental

exists_unique_smul_D_of_transcendental