instAlgebra — Mathlib

English

There is a canonical R-algebra structure on HahnSeries Γ A extending the base algebra via composition with C and the A-algebra structure.

Русский

Существует каноническая структура R-алгебры на HahnSeries Γ A, получаемая путём композиции C с алгебра map R→A и дальнейшими свойствами.

LaTeX

$$$ \text{Algebra}_R(\mathrm{HahnSeries}(\Gamma, A)) $ with $\text{algebraMap} = C \circ \text{algebraMap}_R^A $$$

Lean4

instance : Algebra R (HahnSeries Γ A) where
  algebraMap := C.comp (algebraMap R A)
  smul_def' r
    x := by
    ext
    simp
  commutes' r
    x := by
    ext
    simp only [coeff_smul, single_zero_mul_eq_smul, RingHom.coe_comp, C_apply, Function.comp_apply, algebraMap_smul,
      coeff_mul_single_zero]
    rw [← Algebra.commutes, Algebra.smul_def]

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