oneLePart_one

Mathlib.Algebra.Order.Group.PosPart

URI: https://scilib.ai/kg/mathlib#oneLePart_one

English

The positive part of 1 is 1: (1)⁺ᵐ = 1.

Русский

Положительная часть единицы равна единице: 1⁺ᵐ = 1.

LaTeX

$$$1^{+\!\mathrm{m}} = 1$$$

Lean4

@[to_additive (attr := simp high)]
theorem oneLePart_one : (1 : α)⁺ᵐ = 1 :=
  sup_idem _

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

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

Разделы

Аффилиация

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