smulZeroClass — Mathlib

English

If e: A ≃ B is an equivalence, transporting SMulZeroClass from B to A yields SMulZeroClass on A compatible with e.

Русский

Если e: A ≃ B является эквиваленцией, перенос SMulZeroClass с B на A даёт SMulZeroClass на A, совместимый с e.

LaTeX

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

Lean4

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

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