inv_zero — Mathlib

English

There is a bookkeeping-style Repr instance for CauSeq.Completion.Cauchy, exposing the first few terms of a representative of the equivalence class.

Русский

Имеется экземпляр Repr для CauSeq.Completion.Cauchy, показывающий первые несколько членов представителя класса эквивалентности.

LaTeX

$$$\text{[Repr]}\; (\mathrm{CauSeq.Completion.Cauchy abv})$$$

Lean4

theorem inv_zero : (0 : (Cauchy abv))⁻¹ = 0 :=
  congr_arg mk <| by rw [dif_pos] <;> [rfl; exact zero_limZero]

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