ContainsIdentities — Mathlib

English

A property P of ring homs contains identities if P holds for the identity homomorphism of every ring.

Русский

Свойство P гомоморфов колец содержит идентичности, если P выполняется для тождественного гомоморфа каждого кольца.

LaTeX

$$$\\text{ContainsIdentities} := \\forall R [\\operatorname{CommRing} R], P(\\operatorname{RingHom.id} R).$$$

Lean4

/-- A property `P` of ring homs is said to contain identities if `P` holds
for the identity homomorphism of every ring. -/
def ContainsIdentities :=
  ∀ (R : Type u) [CommRing R], P (RingHom.id R)

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