map_nonunit

Mathlib.NumberTheory.MulChar.Basic

URI: https://scilib.ai/kg/mathlib#MulChar.map_nonunit

English

If χ is a MulChar, then χ(a) = 0 whenever a is not a unit in R.

Русский

Если χ — мульти-char, то χ(a) = 0, когда a не является единицей в R.

LaTeX

$$$\forall a\in R:\ \neg \mathrm{IsUnit}(a) \Rightarrow χ(a)=0.$$$

Lean4

theorem map_nonunit (χ : MulChar R R') {a : R} (ha : ¬IsUnit a) : χ a = 0 :=
  χ.map_nonunit' a ha

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

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

Разделы

Аффилиация

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