inv_one

Mathlib.SetTheory.Game.Basic

URI: https://scilib.ai/kg/mathlib#SetTheory.PGame.inv_one

English

The inverse of 1 is equivalent to 1: 1⁻¹ ≡ 1.

Русский

Обратная к 1 эквивалентна 1: 1⁻¹ ≡ 1.

LaTeX

$$$ 1^{-1} \equiv 1 $$$

Lean4

/-- `1⁻¹` has exactly the same moves as `1`. -/
theorem inv_one : 1⁻¹ ≡ 1 := by
  rw [inv_eq_of_pos PGame.zero_lt_one]
  exact inv'_one

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

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

Разделы

Аффилиация

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