distribMulAction — Mathlib

English

Equivalence e transfers a DistribMulAction structure from B to A, giving DistribMulAction on A compatible with e.

Русский

Эквиваленция e переносит структуру DistribMulAction с B на A, образуя DistribMulAction на A, совместимый с e.

LaTeX

$$$\\text{DistribMulAction}_M A \\cong e^{-1}_{*}(\\text{DistribMulAction}_M B)$$$

Lean4

/-- Transfer `DistribMulAction` across an `Equiv` -/
protected abbrev distribMulAction (e : A ≃ B) [Monoid M] [AddMonoid B] [DistribMulAction M B] :
    letI := e.addMonoid
    DistribMulAction M A :=
  by
  letI := e.addMonoid
  exact { e.distribSMul M, e.mulAction M with }

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