algebraMap_injective

Mathlib.Algebra.QuadraticAlgebra

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

English

The map algebraMap from R to QuadraticAlgebra R a b is injective.

Русский

Отображение algebraMap из R в QuadraticAlgebra R a b инъективно.

LaTeX

$$$\operatorname{algebraMap}\;R\; (\QuadraticAlgebra R a b): R \to (\QuadraticAlgebra R a b)$ is injective$$

Lean4

theorem algebraMap_injective : (algebraMap R (QuadraticAlgebra R a b) : _ → _).Injective := fun _ _ ↦ by
  simp [algebraMap_eq]

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

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

Разделы

Аффилиация

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