mulLeft — Mathlib

English

Reiterates the construction that a subtype defined by a set-like predicate inherits a MulSemiringAction from the ambient action.

Русский

Повторение конструирования: подтип, задаваемый предикатом, наследует MulSemiringAction из общего действия.

LaTeX

$$$\\text{MulSemiringAction (Subtype ...) R}$$$

Lean4

/-- Left multiplication by a unit of a semiring as an additive automorphism. -/
@[simps! +simpRhs]
def mulLeft : Rˣ →* AddAut R :=
  DistribMulAction.toAddAut _ _

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