toTrivSqZeroExt_ι — Mathlib

English

The simp lemma states that the canonical map toTrivSqZeroExt sends ι_R x to TrivSqZeroExt.inr x.

Русский

Лемма-системы упрощения утверждает, что toTrivSqZeroExt отправляет ι_R x в TrivSqZeroExt.inr x.

LaTeX

$$$\mathrm{toTrivSqZeroExt}(\iota_R x) = \mathrm{TrivSqZeroExt.inr}(x)$$$

Lean4

@[simp]
theorem toTrivSqZeroExt_ι [Module Rᵐᵒᵖ M] [IsCentralScalar R M] (x : M) :
    toTrivSqZeroExt (ι R x) = TrivSqZeroExt.inr x :=
  lift_ι_apply _ _ _ _

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