compMulHom_of_isPrimitive — Mathlib

English

If ψ is primitive and f: R' →* R'' is an injective monoid homomorphism, then the composed additive character f ∘ ψ is primitive.

Русский

Если ψ примитивна и f: R' →* R'' инъективно, то составная характеристика f ∘ ψ остаётся примитивной.

LaTeX

$$(f ∘ AddChar ψ).IsPrimitive$$

Lean4

/-- The composition of a primitive additive character with an injective monoid homomorphism
is also primitive. -/
theorem compMulHom_of_isPrimitive {R'' : Type*} [CommMonoid R''] {φ : AddChar R R'} {f : R' →* R''} (hφ : φ.IsPrimitive)
    (hf : Function.Injective f) : (f.compAddChar φ).IsPrimitive := fun a ha ↦ by
  simpa [DFunLike.ext_iff] using (MonoidHom.compAddChar_injective_right f hf).ne (hφ ha)

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