ringHomComp_eq_one_iff — Mathlib

English

If f is injective, then χ.ringHomComp f = 1 iff χ = 1.

Русский

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

LaTeX

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

Lean4

theorem ringHomComp_eq_one_iff {f : R' →+* R''} (hf : Function.Injective f) {χ : MulChar R R'} :
    χ.ringHomComp f = 1 ↔ χ = 1 :=
  by
  conv_lhs => rw [← (show (1 : MulChar R R').ringHomComp f = 1 by simp)]
  exact (injective_ringHomComp hf).eq_iff

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