equivIcoMod_zero — Mathlib

English

For Archimedean α with 0 < p, the equivalence class equivIcoMod hp a 0 is the pair ⟨toIcoMod hp a 0, toIcoMod_mem_Ico hp a 0⟩.

Русский

Для Archimedean α с 0 < p, эквивалентность equivIcoMod hp a 0 равна паре ⟨toIcoMod hp a 0, toIcoMod_mem_Ico hp a 0⟩.

LaTeX

$$QuotientAddGroup.equivIcoMod hp a 0 = ⟨toIcoMod hp a 0, toIcoMod_mem_Ico hp a 0⟩$$

Lean4

@[simp]
theorem equivIcoMod_zero (a : α) : QuotientAddGroup.equivIcoMod hp a 0 = ⟨toIcoMod hp a 0, toIcoMod_mem_Ico hp a _⟩ :=
  rfl

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