ringHomComp_ne_one_iff

Mathlib.NumberTheory.MulChar.Basic

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

← MathLib Explorer

English

χ.ringHomComp f ≠ 1 iff χ ≠ 1, when f is injective.

Русский

χ.ringHomComp f ≠ 1 тогда и только тогда, когда χ ≠ 1, если f инъективен.

LaTeX

$$$$ χ.ringHomComp f \\neq 1 \\iff χ \\neq 1. $$$$

Lean4

theorem ringHomComp_ne_one_iff {f : R' →+* R''} (hf : Function.Injective f) {χ : MulChar R R'} :
    χ.ringHomComp f ≠ 1 ↔ χ ≠ 1 :=
  (ringHomComp_eq_one_iff hf).not

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

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

Разделы

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

Аффилиация

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