coe_eq_one — Mathlib

English

For any character ψ, the underlying function equals 1 if and only if ψ is the zero element: ↑ψ = 1 iff ψ = 0.

Русский

Для любого характерa ψ, совпадает ли функционал с единицей, если и только если ψ — нулевой элемент: ↑ψ = 1 ⇔ ψ = 0.

LaTeX

$$$$ (\uparrow \psi) = 1 \;\Longleftrightarrow\; \psi = 0. $$$$

Lean4

@[simp, norm_cast]
theorem coe_eq_one : ⇑ψ = 1 ↔ ψ = 0 := by rw [← coe_zero, DFunLike.coe_fn_eq]

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