Theorems · Definition · commutative algebra

LaurentSeries.hasseDeriv

(R : Type u_2) →
  {V : Type u_3} →
    [inst : AddCommGroup V] → [inst_1 : Semiring R] → [inst_2 : Module R V] → ℕ → LaurentSeries V →ₗ[R] LaurentSeries V

The Hasse derivative of Laurent series, as a linear map.

Defined in

Mathlib.RingTheory.LaurentSeries

Cited by

9 results in Mathlib

Foundations

Depth 116 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupSemiringModule