ne_one_iff

Mathlib.NumberTheory.MulChar.Basic

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

English

χ ≠ 1 if and only if there exists a unit a with χ(a) ≠ 1.

Русский

χ ≠ 1 тогда и только тогда, когда существует единица a, такая что χ(a) ≠ 1.

LaTeX

$$$$ \\chi \\neq 1 \\ \\iff\\ \\exists a : R^\\times, \\; \\chi(a) \\neq 1. $$$$

Lean4

theorem ne_one_iff {χ : MulChar R R'} : χ ≠ 1 ↔ ∃ a : Rˣ, χ a ≠ 1 := by simp only [Ne, eq_one_iff, not_forall]

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

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

Разделы

Аффилиация

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