toIcoMod_toIcoMod — Mathlib

English

Applying toIcoMod twice is the same as a single application: toIcoMod hp a1 (toIcoMod hp a2 b) = toIcoMod hp a1 b.

Русский

Повторное применение toIcoMod эквивалентно одному: toIcoMod hp a1 (toIcoMod hp a2 b) = toIcoMod hp a1 b.

LaTeX

$$$ toIcoMod\\ hp\\ a1\\ (toIcoMod\\ hp\\ a2\\ b) = toIcoMod\\ hp\\ a1\\ b $$$

Lean4

@[simp]
theorem toIcoMod_toIcoMod (a₁ a₂ b : α) : toIcoMod hp a₁ (toIcoMod hp a₂ b) = toIcoMod hp a₁ b :=
  (toIcoMod_eq_toIcoMod _).2 ⟨toIcoDiv hp a₂ b, self_sub_toIcoMod hp a₂ b⟩

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