instNontrivial_of_right — Mathlib

English

The trivial square-zero extension is nontrivial if the right module is nontrivial and R is nonempty.

Русский

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

LaTeX

$$snd_surjective.nontrivial$$

Lean4

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

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