mul_isClassified — Mathlib

English

For any integer k, if a triple h is classified, then h.mul(k) is classified as well.

Русский

При любом целочисленном k, если тройка h классифицирована, то и тройка h.mul(k) классифицирована.

LaTeX

$$∀ k ∈ ℤ, h.IsClassified ⇒ (h.mul k).IsClassified$$

Lean4

theorem mul_isClassified (k : ℤ) (hc : h.IsClassified) : (h.mul k).IsClassified := by
  obtain ⟨l, m, n, ⟨⟨rfl, rfl⟩ | ⟨rfl, rfl⟩, co⟩⟩ := hc <;> use k * l, m, n <;> grind

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