instDistrib

Mathlib.RingTheory.HahnSeries.Multiplication

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

Lean4

instance [NonUnitalNonAssocSemiring R] : Distrib (HahnSeries Γ R) :=
  { inferInstanceAs (Mul (HahnSeries Γ R)),
    inferInstanceAs
      (Add
        (HahnSeries Γ
          R)) with
    left_distrib := fun x y z => by
      simp only [← of_symm_smul_of_eq_mul]
      exact HahnModule.smul_add x y z
    right_distrib := fun x y z => by
      simp only [← of_symm_smul_of_eq_mul]
      refine HahnModule.add_smul ?_
      simp only [smul_eq_mul]
      exact add_mul }

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

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

Разделы

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

Аффилиация

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