const_ne_one

Mathlib.Algebra.Group.Pi.Lemmas

URI: https://scilib.ai/kg/mathlib#Function.const_ne_one

English

The negation of const_eq_one: const a ≠ 1 if and only if a ≠ 1.

Русский

Лемма о том, что отрицание константной эквивалентности: const a ≠ 1 тогда и только тогда a ≠ 1.

LaTeX

$$$\mathrm{const\_ne\_one} : \; \mathrm{const}_{\iota} a \neq 1 \iff a \neq 1$$$

Lean4

@[to_additive]
theorem const_ne_one : const ι a ≠ 1 ↔ a ≠ 1 :=
  Iff.not const_eq_one

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

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

Разделы

Аффилиация

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