NYLL
Module

CartierCoordinates.lean

Nyll.AlgebraicCurves.Differentials.CartierCoordinates
27 declarations indexed from sourceView source ↗

Module documentation

Cartier Coordinates

Imports3
Imported by6

Declarations

theorem

kw_cart_d_pow_zero

L32 ↗
AlgebraicCurve.KwCart.kw_cart_d_pow_zero
Source context 6 commands

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

open Polynomial IntermediateField AlgebraicCurve.KwPke
noncomputable section
namespace AlgebraicCurve.KwCart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
omit hℓ in
Lean source · statement
theorem kw_cart_d_pow_zero (g : F) :
    KaehlerDifferential.D K F (g ^ ℓ) = 0
theorem

kw_cart_not_pthPower

L36 ↗
AlgebraicCurve.KwCart.kw_cart_not_pthPower
Source context 5 commands

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

open Polynomial IntermediateField AlgebraicCurve.KwPke
noncomputable section
namespace AlgebraicCurve.KwCart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
Lean source · statement
theorem kw_cart_not_pthPower {t : F} (hdt : KaehlerDifferential.D K F t ≠ 0) :
    t ∉ kw_pke_pthPowers F ℓ
theorem

kw_cart_monic_eq_of_associated

L42 ↗
AlgebraicCurve.KwCart.kw_cart_monic_eq_of_associated
Source context 5 commands

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

open Polynomial IntermediateField AlgebraicCurve.KwPke
noncomputable section
namespace AlgebraicCurve.KwCart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
Lean source · statement
theorem kw_cart_monic_eq_of_associated {p q : Polynomial F} (hp : p.Monic) (hq : q.Monic)
    (h : Associated p q) : p = q
theorem

kw_cart_minpoly_natDegree_eq

L51 ↗
AlgebraicCurve.KwCart.kw_cart_minpoly_natDegree_eq
Source context 5 commands

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

open Polynomial IntermediateField AlgebraicCurve.KwPke
noncomputable section
namespace AlgebraicCurve.KwCart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
Lean source · statement
theorem kw_cart_minpoly_natDegree_eq {t : F}
    (hdt : KaehlerDifferential.D K F t ≠ 0) :
    (minpoly (kw_pke_pthPowers F ℓ) t).natDegree = ℓ
theorem

kw_cart_span_singleton_eq_top_of_finrank_one

L123 ↗
AlgebraicCurve.KwCart.kw_cart_span_singleton_eq_top_of_finrank_one
Source context 5 commands

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

open Polynomial IntermediateField AlgebraicCurve.KwPke
noncomputable section
namespace AlgebraicCurve.KwCart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
Lean source · statement
theorem kw_cart_span_singleton_eq_top_of_finrank_one
    {M : Type*} [AddCommGroup M] [Module F M]
    (h1 : Module.finrank F M = 1) {v : M} (hv : v ≠ 0) :
    Submodule.span F {v} = ⊤
theorem

kw_cart_hspan_of_isCurveOver

L131 ↗
AlgebraicCurve.KwCart.kw_cart_hspan_of_isCurveOver
Source context 5 commands

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

open Polynomial IntermediateField AlgebraicCurve.KwPke
noncomputable section
namespace AlgebraicCurve.KwCart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
Lean source · statement
theorem kw_cart_hspan_of_isCurveOver [AlgebraicCurve.IsCurveOver K F] {t : F}
    (hdt : KaehlerDifferential.D K F t ≠ 0) :
    Submodule.span F {KaehlerDifferential.D K F t} = ⊤
theorem

kw_cart_pow_family_indep

L141 ↗
AlgebraicCurve.KwCart.kw_cart_pow_family_indep
Source context 7 commands

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

open Polynomial IntermediateField AlgebraicCurve.KwPke
noncomputable section
namespace AlgebraicCurve.KwCart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
section Repr
variable (t : F)
Lean source · statement
theorem kw_cart_pow_family_indep
    (hdeg : (minpoly (kw_pke_pthPowers F ℓ) t).natDegree = ℓ)
    (c : Fin ℓ → kw_pke_pthPowers F ℓ)
    (h : (∑ i : Fin ℓ, ((c i : F)) * t ^ (i : ℕ)) = 0) :
    ∀ i, c i = 0
theorem

kw_cart_exists_repr

L181 ↗
AlgebraicCurve.KwCart.kw_cart_exists_repr
Source context 7 commands

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

open Polynomial IntermediateField AlgebraicCurve.KwPke
noncomputable section
namespace AlgebraicCurve.KwCart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
section Repr
variable (t : F)
Lean source · statement
theorem kw_cart_exists_repr
    (hsep : ∀ x : F, IsSeparable (kw_pke_expansionField (ℓ := ℓ) t).toSubfield x)
    (hdeg : (minpoly (kw_pke_pthPowers F ℓ) t).natDegree = ℓ)
    (u : F) :
    ∃! c : Fin ℓ → kw_pke_pthPowers F ℓ,
      u = ∑ i : Fin ℓ, ((c i : F)) * t ^ (i : ℕ)
def

kw_cart_repr

L251 ↗
AlgebraicCurve.KwCart.kw_cart_repr
Documentation

The coordinates in the power basis over the subfield of characteristic powers.

Source context 9 commands

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

open Polynomial IntermediateField AlgebraicCurve.KwPke
noncomputable section
namespace AlgebraicCurve.KwCart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
section Repr
variable (t : F)
variable (hsep : ∀ x : F, IsSeparable (kw_pke_expansionField (ℓ := ℓ) t).toSubfield x)
variable (hdeg : (minpoly (kw_pke_pthPowers F ℓ) t).natDegree = ℓ)
Lean source · statement
def kw_cart_repr (u : F) : Fin ℓ → kw_pke_pthPowers F ℓ
theorem

kw_cart_repr_spec

L254 ↗
AlgebraicCurve.KwCart.kw_cart_repr_spec
Source context 9 commands

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

open Polynomial IntermediateField AlgebraicCurve.KwPke
noncomputable section
namespace AlgebraicCurve.KwCart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
section Repr
variable (t : F)
variable (hsep : ∀ x : F, IsSeparable (kw_pke_expansionField (ℓ := ℓ) t).toSubfield x)
variable (hdeg : (minpoly (kw_pke_pthPowers F ℓ) t).natDegree = ℓ)
Lean source · statement
theorem kw_cart_repr_spec (u : F) :
    u = ∑ i : Fin ℓ, ((kw_cart_repr t hsep hdeg u i : F)) * t ^ (i : ℕ)
theorem

kw_cart_repr_unique

L258 ↗
AlgebraicCurve.KwCart.kw_cart_repr_unique
Source context 9 commands

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

open Polynomial IntermediateField AlgebraicCurve.KwPke
noncomputable section
namespace AlgebraicCurve.KwCart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
section Repr
variable (t : F)
variable (hsep : ∀ x : F, IsSeparable (kw_pke_expansionField (ℓ := ℓ) t).toSubfield x)
variable (hdeg : (minpoly (kw_pke_pthPowers F ℓ) t).natDegree = ℓ)
Lean source · statement
theorem kw_cart_repr_unique {u : F} {c : Fin ℓ → kw_pke_pthPowers F ℓ}
    (hc : u = ∑ i : Fin ℓ, ((c i : F)) * t ^ (i : ℕ)) :
    kw_cart_repr t hsep hdeg u = c
theorem

kw_cart_repr_add

L264 ↗
AlgebraicCurve.KwCart.kw_cart_repr_add
Source context 9 commands

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

open Polynomial IntermediateField AlgebraicCurve.KwPke
noncomputable section
namespace AlgebraicCurve.KwCart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
section Repr
variable (t : F)
variable (hsep : ∀ x : F, IsSeparable (kw_pke_expansionField (ℓ := ℓ) t).toSubfield x)
variable (hdeg : (minpoly (kw_pke_pthPowers F ℓ) t).natDegree = ℓ)
Lean source · statement
theorem kw_cart_repr_add (u v : F) :
    kw_cart_repr t hsep hdeg (u + v)
      = kw_cart_repr t hsep hdeg u + kw_cart_repr t hsep hdeg v
theorem

kw_cart_repr_pow_smul

L283 ↗
AlgebraicCurve.KwCart.kw_cart_repr_pow_smul
Source context 9 commands

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

open Polynomial IntermediateField AlgebraicCurve.KwPke
noncomputable section
namespace AlgebraicCurve.KwCart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
section Repr
variable (t : F)
variable (hsep : ∀ x : F, IsSeparable (kw_pke_expansionField (ℓ := ℓ) t).toSubfield x)
variable (hdeg : (minpoly (kw_pke_pthPowers F ℓ) t).natDegree = ℓ)
Lean source · full declaration
theorem kw_cart_repr_pow_smul (a : F) (u : F) :
    kw_cart_repr t hsep hdeg (a ^ ℓ * u)
      = fun i => ⟨a ^ ℓ, (kw_pke_mem_pthPowers_iff F ℓ).mpr ⟨a, rfl⟩⟩
          * kw_cart_repr t hsep hdeg u i := by
  refine kw_cart_repr_unique t hsep hdeg ?_
  have hu := kw_cart_repr_spec t hsep hdeg u
  calc a ^ ℓ * u
      = a ^ ℓ * ∑ i : Fin ℓ, ((kw_cart_repr t hsep hdeg u i : F)) * t ^ (i : ℕ) := by
        rw [← hu]
    _ = ∑ i : Fin ℓ,
          (((fun i => (⟨a ^ ℓ, (kw_pke_mem_pthPowers_iff F ℓ).mpr ⟨a, rfl⟩⟩ :
              kw_pke_pthPowers F ℓ) * kw_cart_repr t hsep hdeg u i) i : F))
            * t ^ (i : ℕ) := by
        rw [Finset.mul_sum]
        refine Finset.sum_congr rfl fun i _ => ?_
        push_cast
        ring
def

kw_cart_root

L306 ↗
AlgebraicCurve.KwCart.kw_cart_root
Documentation

A chosen characteristic root of an element of the subfield of characteristic powers.

Source context 6 commands

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

open Polynomial IntermediateField AlgebraicCurve.KwPke
noncomputable section
namespace AlgebraicCurve.KwCart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
section Root
Lean source · statement
def kw_cart_root (p : kw_pke_pthPowers F ℓ) : F
theorem

kw_cart_root_pow

L309 ↗
AlgebraicCurve.KwCart.kw_cart_root_pow
Source context 6 commands

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

open Polynomial IntermediateField AlgebraicCurve.KwPke
noncomputable section
namespace AlgebraicCurve.KwCart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
section Root
Lean source · statement
theorem kw_cart_root_pow (p : kw_pke_pthPowers F ℓ) :
    (kw_cart_root p) ^ ℓ = (p : F)
theorem

kw_cart_root_unique

L313 ↗
AlgebraicCurve.KwCart.kw_cart_root_unique
Source context 6 commands

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

open Polynomial IntermediateField AlgebraicCurve.KwPke
noncomputable section
namespace AlgebraicCurve.KwCart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
section Root
Lean source · statement
theorem kw_cart_root_unique {p : kw_pke_pthPowers F ℓ} {g : F}
    (hg : g ^ ℓ = (p : F)) : kw_cart_root p = g
theorem

kw_cart_root_add

L319 ↗
AlgebraicCurve.KwCart.kw_cart_root_add
Source context 6 commands

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

open Polynomial IntermediateField AlgebraicCurve.KwPke
noncomputable section
namespace AlgebraicCurve.KwCart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
section Root
Lean source · statement
theorem kw_cart_root_add (p q : kw_pke_pthPowers F ℓ) :
    kw_cart_root (p + q) = kw_cart_root p + kw_cart_root q
theorem

kw_cart_root_pow_mul

L325 ↗
AlgebraicCurve.KwCart.kw_cart_root_pow_mul
Source context 6 commands

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

open Polynomial IntermediateField AlgebraicCurve.KwPke
noncomputable section
namespace AlgebraicCurve.KwCart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
section Root
Lean source · statement
theorem kw_cart_root_pow_mul (a : F) (p : kw_pke_pthPowers F ℓ) :
    kw_cart_root (⟨a ^ ℓ, (kw_pke_mem_pthPowers_iff F ℓ).mpr ⟨a, rfl⟩⟩ * p)
      = a * kw_cart_root p
theorem

kw_cart_exists_dtCoord

L336 ↗
AlgebraicCurve.KwCart.kw_cart_exists_dtCoord
Source context 6 commands

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

open Polynomial IntermediateField AlgebraicCurve.KwPke
noncomputable section
namespace AlgebraicCurve.KwCart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
section Cartier
Lean source · statement
theorem kw_cart_exists_dtCoord (t : F) (hdt : KaehlerDifferential.D K F t ≠ 0)
    (hspan : Submodule.span F {KaehlerDifferential.D K F t} = ⊤)
    (ω : Ω[F⁄K]) : ∃! w : F, ω = w • KaehlerDifferential.D K F t
def

kw_cart_dtCoord

L352 ↗
AlgebraicCurve.KwCart.kw_cart_dtCoord
Documentation

The coefficient of a differential with respect to the differential of the chosen coordinate.

Source context 6 commands

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

open Polynomial IntermediateField AlgebraicCurve.KwPke
noncomputable section
namespace AlgebraicCurve.KwCart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
section Cartier
Lean source · statement
def kw_cart_dtCoord (t : F) (hdt : KaehlerDifferential.D K F t ≠ 0)
    (hspan : Submodule.span F {KaehlerDifferential.D K F t} = ⊤) (ω : Ω[F⁄K]) : F
theorem

kw_cart_dtCoord_spec

L356 ↗
AlgebraicCurve.KwCart.kw_cart_dtCoord_spec
Source context 6 commands

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

open Polynomial IntermediateField AlgebraicCurve.KwPke
noncomputable section
namespace AlgebraicCurve.KwCart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
section Cartier
Lean source · statement
theorem kw_cart_dtCoord_spec (t : F) (hdt : KaehlerDifferential.D K F t ≠ 0)
    (hspan : Submodule.span F {KaehlerDifferential.D K F t} = ⊤) (ω : Ω[F⁄K]) :
    ω = kw_cart_dtCoord t hdt hspan ω • KaehlerDifferential.D K F t
theorem

kw_cart_dtCoord_unique

L361 ↗
AlgebraicCurve.KwCart.kw_cart_dtCoord_unique
Source context 6 commands

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

open Polynomial IntermediateField AlgebraicCurve.KwPke
noncomputable section
namespace AlgebraicCurve.KwCart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
section Cartier
Lean source · statement
theorem kw_cart_dtCoord_unique (t : F) (hdt : KaehlerDifferential.D K F t ≠ 0)
    (hspan : Submodule.span F {KaehlerDifferential.D K F t} = ⊤) {ω : Ω[F⁄K]} {w : F}
    (hw : ω = w • KaehlerDifferential.D K F t) :
    kw_cart_dtCoord t hdt hspan ω = w
theorem

kw_cart_dtCoord_add

L372 ↗
AlgebraicCurve.KwCart.kw_cart_dtCoord_add
Source context 6 commands

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

open Polynomial IntermediateField AlgebraicCurve.KwPke
noncomputable section
namespace AlgebraicCurve.KwCart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
section Cartier
Lean source · statement
theorem kw_cart_dtCoord_add (t : F) (hdt : KaehlerDifferential.D K F t ≠ 0)
    (hspan : Submodule.span F {KaehlerDifferential.D K F t} = ⊤) (ω ω' : Ω[F⁄K]) :
    kw_cart_dtCoord t hdt hspan (ω + ω')
      = kw_cart_dtCoord t hdt hspan ω + kw_cart_dtCoord t hdt hspan ω'
theorem

kw_cart_dtCoord_smul

L382 ↗
AlgebraicCurve.KwCart.kw_cart_dtCoord_smul
Source context 6 commands

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

open Polynomial IntermediateField AlgebraicCurve.KwPke
noncomputable section
namespace AlgebraicCurve.KwCart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
section Cartier
Lean source · statement
theorem kw_cart_dtCoord_smul (t : F) (hdt : KaehlerDifferential.D K F t ≠ 0)
    (hspan : Submodule.span F {KaehlerDifferential.D K F t} = ⊤) (a : F) (ω : Ω[F⁄K]) :
    kw_cart_dtCoord t hdt hspan (a • ω) = a * kw_cart_dtCoord t hdt hspan ω
def

kw_cart_C

L392 ↗
AlgebraicCurve.KwCart.kw_cart_C
Documentation

The Cartier operator in the chosen coordinate, obtained from the final power-basis coefficient.

Source context 6 commands

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

open Polynomial IntermediateField AlgebraicCurve.KwPke
noncomputable section
namespace AlgebraicCurve.KwCart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
section Cartier
Lean source · statement
def kw_cart_C (t : F) (hdt : KaehlerDifferential.D K F t ≠ 0)
    (hspan : Submodule.span F {KaehlerDifferential.D K F t} = ⊤)
    (hsep : ∀ x : F, IsSeparable (kw_pke_expansionField (ℓ := ℓ) t).toSubfield x)
    (hdeg : (minpoly (kw_pke_pthPowers F ℓ) t).natDegree = ℓ)
    (ω : Ω[F⁄K]) : Ω[F⁄K]
theorem

kw_cart_C_add

L400 ↗
AlgebraicCurve.KwCart.kw_cart_C_add
Source context 6 commands

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

open Polynomial IntermediateField AlgebraicCurve.KwPke
noncomputable section
namespace AlgebraicCurve.KwCart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
section Cartier
Lean source · statement
theorem kw_cart_C_add (t : F) (hdt : KaehlerDifferential.D K F t ≠ 0)
    (hspan : Submodule.span F {KaehlerDifferential.D K F t} = ⊤)
    (hsep : ∀ x : F, IsSeparable (kw_pke_expansionField (ℓ := ℓ) t).toSubfield x)
    (hdeg : (minpoly (kw_pke_pthPowers F ℓ) t).natDegree = ℓ)
    (ω ω' : Ω[F⁄K]) :
    kw_cart_C (K := K) t hdt hspan hsep hdeg (ω + ω')
      = kw_cart_C (K := K) t hdt hspan hsep hdeg ω
        + kw_cart_C (K := K) t hdt hspan hsep hdeg ω'
theorem

kw_cart_C_semilinear

L416 ↗
AlgebraicCurve.KwCart.kw_cart_C_semilinear
Source context 6 commands

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

open Polynomial IntermediateField AlgebraicCurve.KwPke
noncomputable section
namespace AlgebraicCurve.KwCart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP F ℓ]
section Cartier
Lean source · statement
theorem kw_cart_C_semilinear (t : F) (hdt : KaehlerDifferential.D K F t ≠ 0)
    (hspan : Submodule.span F {KaehlerDifferential.D K F t} = ⊤)
    (hsep : ∀ x : F, IsSeparable (kw_pke_expansionField (ℓ := ℓ) t).toSubfield x)
    (hdeg : (minpoly (kw_pke_pthPowers F ℓ) t).natDegree = ℓ)
    (a : F) (ω : Ω[F⁄K]) :
    kw_cart_C (K := K) t hdt hspan hsep hdeg (a ^ ℓ • ω)
      = a • kw_cart_C (K := K) t hdt hspan hsep hdeg ω

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.