nontrivial — Mathlib

English

If R is a nontrivial ring and A is a bialgebra over R, then A is nontrivial (i.e., not the zero ring).

Русский

Если R — ненулевое кольцо и A — биалгебра над R, то A ненулева. (A не нулевой кольцо).

LaTeX

$$$\\exists a,b \\in A\\; (a \\neq b)$$$

Lean4

/-- A bialgebra over a nontrivial ring is nontrivial. -/
theorem nontrivial [Nontrivial R] : Nontrivial A :=
  (algebraMap_injective (R := R) _).nontrivial

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