instMulSemiringActionQuotientOfIsScalarTower

English

The quotient RingCon inherits a MulSemiringAction of α, i.e., the scalar action respects both multiplication and one, i.e., smul_one and smul_mul properties hold in the quotient.

Русский

Фактор RingCon наследует MulSemiringAction от α: скаляры сохраняют умножение и единицу в факторе, выполняются smul_one и smul_mul.

LaTeX

$$$$ \\text{smul\_one} \\quad \\text{and} \\quad \\text{smul\_mul} $$$$

Lean4

instance [Monoid α] [Semiring R] [MulSemiringAction α R] [IsScalarTower α R R] (c : RingCon R) :
    MulSemiringAction α c.Quotient :=
  { smul_one := fun _ => congr_arg toQuotient <| smul_one _
    smul_mul := fun _ => Quotient.ind₂' fun _ _ => congr_arg toQuotient <| MulSemiringAction.smul_mul _ _ _ }

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