instNontrivial_of_left — Mathlib

English

The trivial square-zero extension is nontrivial if the left ring is nontrivial and M is nonempty.

Русский

Тривиальное квадратное дополнение не тождественно, если левая компонента кольца ненулевая, а M непусто.

LaTeX

$$fst_surjective.nontrivial$$

Lean4

/-- The trivial square-zero extension is nontrivial if it is over a nontrivial ring. -/
instance instNontrivial_of_left {R M : Type*} [Nontrivial R] [Nonempty M] : Nontrivial (TrivSqZeroExt R M) :=
  fst_surjective.nontrivial

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