distribSMul — Mathlib

English

An equivalence e transfers DistribSMul from B to A, yielding a DistribSMul on A with smul_add adjusted by e.

Русский

Через эквиваленцию e переносится DistribSMul с B на A, образуя DistribSMul на A с поправкой на smul_add.

LaTeX

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

Lean4

/-- Transfer `DistribSMul` across an `Equiv` -/
protected abbrev distribSMul (e : A ≃ B) [AddZeroClass B] [DistribSMul M B] :
    letI := e.addZeroClass
    DistribSMul M A :=
  by
  letI := e.addZeroClass
  exact { e.smulZeroClass M with smul_add := by simp [add_def, smul_def, smul_add] }

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