toDistribMulActionHom — Mathlib

English

From any σ-semi-linear map f one obtains a DistribMulActionHom σ.toMonoidHom M M3, whose underlying function is f and which satisfies the zero-preserving property.

Русский

Из любого σ-симилинейного отображения f получается DistribMulActionHom σ.toMonoidHom M M3, чья базовая функция равна f и который сохраняет нуль.

LaTeX

$$$(\mathrm{toDistribMulActionHom}(f)).\toFun = f \quad\land\quad (\mathrm{toDistribMulActionHom}(f)).map_zero' = \mathrm{map_zero}(f)$$$

Lean4

/-- The `DistribMulActionHom` underlying a `LinearMap`. -/
def toDistribMulActionHom (f : M →ₛₗ[σ] M₃) : DistribMulActionHom σ.toMonoidHom M M₃ :=
  { f with map_zero' := show f 0 = 0 from map_zero f }

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