instNontrivialLeft — Mathlib

English

If the base field is nontrivial and the right factor is nonempty, then Unitization is nontrivial.

Русский

Если основание не тривиально и правая компонента не пустая, то Unitization не тривиальна.

LaTeX

$$$[Nontrivial 𝕜], [Nonempty A] \\\\Rightarrow Nontrivial (Unitization 𝕜 A).$$$

Lean4

instance instNontrivialLeft {𝕜 A} [Nontrivial 𝕜] [Nonempty A] : Nontrivial (Unitization 𝕜 A) :=
  nontrivial_prod_left

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