Theorems · Theorem · ring theory

RingHom.domain_nontrivial

∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) [Nontrivial β],
  Nontrivial α

If there is a homomorphism f : α →+* β and β is nontrivial, then α is nontrivial.

Defined in

Mathlib.Algebra.Ring.Hom.Defs

Cited by

20 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext

Assumes

Nontrivial