toSubsemiring_subtype

Mathlib.Algebra.Algebra.Subalgebra.Basic

URI: https://scilib.ai/kg/mathlib#Subalgebra.toSubsemiring_subtype

English

The subsemiring structure induced by S coincides with the subtype structure of S as a subset of A.

Русский

Структура подполосы Subsemiring, индукции S, совпадает с подсистемой подмножества S в A.

LaTeX

$$$S.toSubsemiring.subtype = (S.val : S \to+* A)$$$

Lean4

@[simp]
theorem toSubsemiring_subtype : S.toSubsemiring.subtype = (S.val : S →+* A) :=
  rfl

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

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

Разделы

Аффилиация

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