nonUnitalNonAssocSemiring — Mathlib

English

Equivalence between idempotence of q − p and the equalities p q = p and q p = p given p,q idempotent in a ring with IsAddTorsionFree.

Русский

Эквивалентность идемпотентности q−p и равенств p q = p, q p = p при p,q идемпотентны.

LaTeX

$$IsIdempotentElem (q - p) ↔ p q = p ∧ q p = p$$

Lean4

/-- Pullback a `NonUnitalNonAssocSemiring` instance along an injective function. -/
-- See note [reducible non-instances]

protected abbrev nonUnitalNonAssocSemiring [NonUnitalNonAssocSemiring R] (zero : f 0 = 0)
    (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) : NonUnitalNonAssocSemiring S
    where
  toAddCommMonoid := hf.addCommMonoid f zero add (swap nsmul)
  __ := hf.distrib f add mul
  __ := hf.mulZeroClass f zero mul

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