one_apply_eq_zero_iff — Mathlib

English

For all x, (1 : M₀ →*₀ N₀) x = 0 iff x = 0.

Русский

Для всех x верно: (1 : M₀ →*₀ N₀) x = 0 ↔ x = 0.

LaTeX

$$$(1 : M_0 \\to^*₀ N_0)\\, x = 0 \\iff x = 0$$$

Lean4

@[simp]
theorem one_apply_eq_zero_iff {M₀ N₀ : Type*} [MulZeroOneClass M₀] [MulZeroOneClass N₀]
    [DecidablePred fun x : M₀ ↦ x = 0] [Nontrivial M₀] [NoZeroDivisors M₀] [Nontrivial N₀] {x : M₀} :
    (1 : M₀ →*₀ N₀) x = 0 ↔ x = 0 := by rcases eq_or_ne x 0 with rfl | hx <;> simp_all [one_apply_of_ne_zero]

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