one_mul — Mathlib

English

1 * x is equivalent to x.

Русский

Единица слева умножения на x эквивалентна x.

LaTeX

$$1 \cdot x \equiv x$$

Lean4

/-- `1 * x` has the same moves as `x`. -/
protected theorem one_mul : ∀ (x : PGame), 1 * x ≡ x
  | ⟨xl, xr, xL, xR⟩ => by
    refine
        Identical.of_equiv ((Equiv.sumEmpty _ _).trans (Equiv.punitProd _))
          ((Equiv.sumEmpty _ _).trans (Equiv.punitProd _)) ?_ ?_ <;>
      · rintro (⟨⟨⟩, _⟩ | ⟨⟨⟩, _⟩)
        exact
          ((((PGame.zero_mul (mk _ _ _ _)).add (PGame.one_mul _)).trans (PGame.zero_add _)).sub
                (PGame.zero_mul _)).trans
            (PGame.sub_zero _)

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