instNonUnitalCommSemiring

Mathlib.RingTheory.HahnSeries.Multiplication

URI: https://scilib.ai/kg/mathlib#HahnSeries.instNonUnitalCommSemiring

Lean4

instance [NonUnitalCommSemiring R] : NonUnitalCommSemiring (HahnSeries Γ R)
    where
  __ : NonUnitalSemiring (HahnSeries Γ R) := inferInstance
  mul_comm x
    y := by
    ext
    simp_rw [coeff_mul, mul_comm]
    exact Finset.sum_equiv (Equiv.prodComm _ _) (fun _ ↦ swap_mem_addAntidiagonal.symm) <| by simp

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru