principal_mul_two

Mathlib.SetTheory.Ordinal.Principal

URI: https://scilib.ai/kg/mathlib#Ordinal.principal_mul_two

← MathLib Explorer

English

2 is a principal for multiplication: Principal (· * ·) 2.

Русский

2 является принципиальным для умножения: Principal (· * ·) 2.

LaTeX

$$$Principal(\cdot * \cdot, 2).$$$

Lean4

theorem principal_mul_two : Principal (· * ·) 2 := by
  intro a b ha hb
  rw [← succ_one, lt_succ_iff] at *
  convert mul_le_mul' ha hb
  exact (mul_one 1).symm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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