fstHom

Mathlib.Algebra.TrivSqZeroExt

URI: https://scilib.ai/kg/mathlib#TrivSqZeroExt.fstHom

← MathLib Explorer

English

For x with fst ≠ 0, x · x^{-1} = 1.

Русский

Для x с fst(x) ≠ 0 выполняется x · x^{-1} = 1.

LaTeX

$$$ fst(x) \\neq 0 \\Rightarrow x \\cdot x^{-1} = 1 $$$

Lean4

/-- The canonical `S`-algebra projection `TrivSqZeroExt R M → R`. -/
@[simps]
def fstHom : tsze R M →ₐ[S] R where
  toFun := fst
  map_one' := fst_one
  map_mul' := fst_mul
  map_zero' := fst_zero (M := M)
  map_add' := fst_add
  commutes' _r := fst_inl M _

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru