mulDistribMulAction — Mathlib

English

If e: N ≃ O is an equivalence and M acts on O by MulDistribMulAction, then the transported action defines a MulDistribMulAction of M on N.

Русский

Если e: N ≃ O — эквивалент, и M действует на O по MulDistribMulAction, то перемещённое действие задаёт MulDistribMulAction M на N.

LaTeX

$$$\\forall e:\\, N \\simeq O,\\ [\\operatorname{MulDistribMulAction} M\, O] \\Rightarrow \\operatorname{MulDistribMulAction} M\, N$$$

Lean4

/-- Transfer `MulDistribMulAction` across an `Equiv` -/
protected abbrev mulDistribMulAction (e : N ≃ O) [MulDistribMulAction M O] :
    letI := e.monoid
    MulDistribMulAction M N :=
  letI := e.monoid
  { e.mulAction M with
    smul_one := by simp [one_def, smul_def, smul_one]
    smul_mul := by simp [mul_def, smul_def, smul_mul'] }

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