isMultiplicative — Mathlib

English

If Q is stable under composition and contains identities, then the associated scheme-property P is multiplicative: it is closed under composition and includes identity morphisms.

Русский

Если Q устойчива к композиции и содержит тождественные гомоморфизм, то соответствующее свойство схем P мультпликтативно: оно сохраняется при композиции и содержит тождественные морфизмы.

LaTeX

$$$(\text{RingHom.StableUnderComposition } Q) \land (\text{RingHom.ContainsIdentities } Q) \Rightarrow P.IsMultiplicative.$$$

Lean4

theorem isMultiplicative (hPc : RingHom.StableUnderComposition Q) (hPi : RingHom.ContainsIdentities Q) :
    P.IsMultiplicative where
  comp_mem := (stableUnderComposition hPc).comp_mem
  id_mem := (containsIdentities hPi).id_mem

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