instNontrivial

Mathlib.Algebra.QuadraticAlgebra

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

English

If R is nontrivial, then QuadraticAlgebra R a b is nontrivial.

Русский

Если R не тривиальна, то QuadraticAlgebra R a b не тривиальна.

LaTeX

$$$\\forall R:\\, [\\text{Nontrivial }R] \\Rightarrow [\\text{Nontrivial }(\\ QuadraticAlgebra R a b)].$$$

Lean4

instance [Nontrivial R] : Nontrivial (QuadraticAlgebra R a b) :=
  (equivProd a b).nontrivial

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

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

Разделы

Аффилиация

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