instNonTrivial — Mathlib

English

There is a well-defined inversion operation on nonzero elements of CauSeq.Completion.Cauchy abv, giving a multiplicative inverse within the completion.

Русский

Для ненулевых элементов CauSeq.Completion.Cauchy abv определена операция взятия обратной, дающая умножение-обратное внутри дополнения.

LaTeX

$$$x \neq 0 \Rightarrow x^{-1} \in \mathrm{CauSeq.Completion.Cauchy}\ abv$ и $x \cdot x^{-1} = 1$ в рамках завершения.$$

Lean4

noncomputable instance instNonTrivial [Nontrivial β] : Nontrivial (Cauchy abv) :=
  ofRat_injective.nontrivial

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