smulWithZero — Mathlib

English

Via an equivalence e, transfer SMulWithZero from B to A to obtain a SMulWithZero on A compatible with e.

Русский

Через эквиваленцию e переносим SMulWithZero с B на A, получая SMulWithZero на A, совместимый с e.

LaTeX

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

Lean4

/-- Transfer `SMulWithZero` across an `Equiv` -/
protected abbrev smulWithZero (e : A ≃ B) [Zero M₀] [Zero B] [SMulWithZero M₀ B] :
    letI := e.zero
    SMulWithZero M₀ A :=
  by
  letI := e.zero
  exact { e.smulZeroClass M₀ with zero_smul := by simp [smul_def, zero_def] }

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