instNontrivial

Mathlib.Analysis.Normed.Ring.WithAbs

URI: https://scilib.ai/kg/mathlib#WithAbs.instNontrivial

English

If R is nontrivial, then WithAbs v is nontrivial.

Русский

Если R нетривиально, то WithAbs v нетривиально.

LaTeX

$$Nontrivial(R) \\Rightarrow Nontrivial(WithAbs(v))$$

Lean4

instance instNontrivial [Nontrivial R] : Nontrivial (WithAbs v) :=
  inferInstanceAs (Nontrivial R)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru