Theorems · Definition · commutative algebra

HahnModule

(Γ : Type u_6) → (R : Type u_7) → (V : Type u_8) → [PartialOrder Γ] → [Zero V] → [SMul R V] → Type (max u_6 u_8)

We introduce a type alias for HahnSeries in order to work with scalar multiplication by series. If we wrote a SMul R⟦Γ⟧ V⟦Γ⟧ instance, then when V = R⟦Γ⟧, we would have two different actions of R⟦Γ⟧ on V⟦Γ⟧. See Mathlib/Algebra/Polynomial/Module/Basic.lean for more discussion on this problem.

Defined in

Mathlib.RingTheory.HahnSeries.Multiplication

Cited by

51 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

PartialOrderZeroSMul