toSemiring_injective

Mathlib.Algebra.Ring.Ext

URI: https://scilib.ai/kg/mathlib#Ring.toSemiring_injective

← MathLib Explorer

English

The map toSemiring from Ring is injective.

Русский

Отображение toSemiring от Ring инъективно.

LaTeX

$$$\\\\forall A,B \\,\\in \\, \\text{Ring}(R), \\\\ toSemiring(A) = toSemiring(B) \\\\Rightarrow A = B.$$$

Lean4

theorem toSemiring_injective : Function.Injective (@toSemiring R) :=
  by
  intro _ _ h
  ext x y
  · exact congrArg (·.toAdd.add x y) h
  · exact congrArg (·.toMul.mul x y) h

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

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

Разделы

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

Аффилиация

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