Theorems · Theorem · commutative algebra

HahnSeries.single_pow

∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : Semiring R] (a : Γ) (n : ℕ) (r : R), (HahnSeries.single a) r ^ n = (HahnSeries.single (n • a)) (r ^ n)

Defined in

Mathlib.RingTheory.HahnSeries.Multiplication

Cited by

5 results in Mathlib

Foundations

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

Assumes

AddCommMonoidPartialOrderIsOrderedCancelAddMonoidSemiring