nmul_one — Mathlib

English

Multiplying by one on the right leaves the left operand unchanged: a ⨳ 1 = a.

Русский

Умножение справа на единицу не изменяет левый операнд: a ⨳ 1 = a.

LaTeX

$$$\\forall a \\in \\mathrm{Ordinal},\\ a \\nabla 1 = a$$$

Lean4

@[simp]
theorem nmul_one (a : Ordinal) : a ⨳ 1 = a := by
  rw [nmul]
  convert csInf_Ici
  ext b
  refine ⟨fun H ↦ le_of_forall_lt (a := a) fun c hc ↦ ?_, fun ha c hc ↦ ?_⟩
  · simpa [nmul_one c] using H c hc
  · simpa [nmul_one c] using hc.trans_le ha
termination_by a

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