instNontrivial

Mathlib.LinearAlgebra.SymmetricAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#SymmetricAlgebra.instNontrivial

← MathLib Explorer

English

If R is nontrivial, then SymmetricAlgebra R M is nontrivial as well.

Русский

Если R не тривиальна, то и SymmetricAlgebra R M также не тривиальна.

LaTeX

$$$[\text{Nontrivial } R] \Rightarrow [\text{Nontrivial } \operatorname{Sym}_R(M)].$$$

Lean4

/-- A `SymmetricAlgebra` over a nontrivial semiring is nontrivial. -/
instance [Nontrivial R] : Nontrivial (SymmetricAlgebra R M) :=
  (algebraMap_leftInverse M).injective.nontrivial

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

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

Разделы

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

Аффилиация

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