toSubsemigroup_strictMono

Mathlib.RingTheory.NonUnitalSubsemiring.Basic

URI: https://scilib.ai/kg/mathlib#NonUnitalSubsemiring.toSubsemigroup_strictMono

English

The map toSubsemigroup is strictly monotone: StrictMono (toSubsemigroup).

Русский

Отображение toSubsemigroup строго монотонно: StrictMono (toSubsemigroup).

LaTeX

$$$\text{StrictMono} (\text{toSubsemigroup} : \text{NonUnitalSubsemiring } R \to \text{Subsemigroup } R)$$$

Lean4

@[mono]
theorem toSubsemigroup_strictMono : StrictMono (toSubsemigroup : NonUnitalSubsemiring R → Subsemigroup R) := fun _ _ =>
  id

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

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

Разделы

Аффилиация

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