toAddSubmonoid_strictMono

Mathlib.RingTheory.NonUnitalSubsemiring.Basic

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

English

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

Русский

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

LaTeX

$$$\text{StrictMono} (\text{toAddSubmonoid} : \text{NonUnitalSubsemiring } R \to \text{AddSubmonoid } R)$$$

Lean4

@[mono]
theorem toAddSubmonoid_strictMono : StrictMono (toAddSubmonoid : NonUnitalSubsemiring R → AddSubmonoid R) := fun _ _ =>
  id

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

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

Разделы

Аффилиация

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