codomain_trivial_iff_range_trivial

English

A ring hom has trivial codomain iff its range is trivial.

Русский

Кольцевый гомоморфизм имеет тривиальный кодоморфизм кольца тогда и только тогда, когда область значений тривиальна.

LaTeX

$$$(0:\beta)=1 \Longleftrightarrow \forall x, f(x)=0$$$

Lean4

/-- `f : α →+* β` has a trivial codomain iff it has a trivial range. -/
theorem codomain_trivial_iff_range_trivial : (0 : β) = 1 ↔ ∀ x, f x = 0 :=
  f.codomain_trivial_iff_map_one_eq_zero.trans ⟨fun h x => by rw [← mul_one x, map_mul, h, mul_zero], fun h => h 1⟩

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