comp — Mathlib

English

Composition with a ring homomorphism preserves the IsQuadratic property: if χ is quadratic, then χ.ringHomComp f is quadratic.

Русский

Композиция с кольцевым гомоморфизмом сохраняет свойство квадратичности: если χ квадратичный, то χ.ringHomComp f квадратичен.

LaTeX

$$$$ (\\chi.ringHomComp f).IsQuadratic. $$$$

Lean4

/-- Composition with a ring homomorphism preserves the property of being a quadratic character. -/
theorem comp {χ : MulChar R R'} (hχ : χ.IsQuadratic) (f : R' →+* R'') : (χ.ringHomComp f).IsQuadratic :=
  by
  intro a
  rcases hχ a with (ha | ha | ha) <;> simp [ha]

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