equivIocMod_zero — Mathlib

English

There is a canonical identification of the zero coset with the interval IocMod hp a 0.

Русский

Существует каноническое отображение нулевой косеты в интервал IocMod hp a 0.

LaTeX

$$$$ \operatorname{equivIocMod}(hp, a)(0) = \langle \operatorname{toIocMod}(hp, a, 0), \operatorname{toIocMod\_mem\_Ioc}(hp, a, 0) \rangle $$$$

Lean4

@[simp]
theorem equivIocMod_zero (a : α) : QuotientAddGroup.equivIocMod hp a 0 = ⟨toIocMod hp a 0, toIocMod_mem_Ioc hp a _⟩ :=
  rfl

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