coe_ne_zero

Mathlib.Algebra.Group.AddChar

URI: https://scilib.ai/kg/mathlib#AddChar.coe_ne_zero

← MathLib Explorer

English

The underlying function (ψ : A → M₀) is not identically zero.

Русский

Обозначение (ψ : A → M₀) не является нулевой функцией.

LaTeX

$$$ (\psi : A \to M_0) \neq 0$$$

Lean4

@[simp]
theorem coe_ne_zero (ψ : AddChar A M₀) : (ψ : A → M₀) ≠ 0 :=
  ne_iff.2 ⟨0, fun h ↦ by simpa only [h, Pi.zero_apply, zero_ne_one] using map_zero_eq_one ψ⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru