isNontrivial_congr — Mathlib

English

If v.IsNontrivial and h is a congruence between v and w, then v and w share the same nontriviality property; in particular, they agree on the presence of nonzero values.

Русский

Если v не тривиально и есть конгруэнтность между v и w, то они имеют одинаковую ненулевую характеристику; следовательно, они согласованы по существованию ненулевых значений.

LaTeX

$$$ \text{If } v \text{ is nontrivial and } h: v \cong w, \\ v \text{ nontrivial } \iff w \text{ nontrivial }$$$

Lean4

theorem isNontrivial_congr {w : AbsoluteValue R S} (h : v.IsEquiv w) : v.IsNontrivial ↔ w.IsNontrivial :=
  not_iff_not.1 <| by aesop (add simp [not_isNontrivial_iff, h.eq_one_iff])

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