mulActionWithZero — Mathlib

English

An equivalence e transfers MulActionWithZero from B to A, giving a MulActionWithZero on A compatible with e.

Русский

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

LaTeX

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

Lean4

/-- Transfer `MulActionWithZero` across an `Equiv` -/
protected abbrev mulActionWithZero (e : A ≃ B) [MonoidWithZero M₀] [Zero B] [MulActionWithZero M₀ B] :
    letI := e.zero
    MulActionWithZero M₀ A :=
  by
  letI := e.zero
  exact { e.smulWithZero M₀, e.mulAction M₀ with }

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