domain_nontrivial — Mathlib

English

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

Русский

Если существует кольцевой гомоморфизм f: α →+* β и β ненулевой, то α ненулевой.

LaTeX

$$(∃ f: α →+* β) [Nontrivial β] ⇒ Nontrivial α$$

Lean4

/-- If there is a homomorphism `f : α →+* β` and `β` is nontrivial, then `α` is nontrivial. -/
theorem domain_nontrivial [Nontrivial β] : Nontrivial α :=
  ⟨⟨1, 0, mt (fun h => show f 1 = 0 by rw [h, map_zero]) f.map_one_ne_zero⟩⟩

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