pushoutDesc_left — Mathlib

English

In a pushout, the left leg composed with pushoutDesc evaluates to f on S-elements.

Русский

В пушауте левая ножка, после композиции pushoutDesc, дает f на элементах S.

LaTeX

$$Algebra.pushoutDesc_left S' f g H x = f x$$

Lean4

@[simp]
theorem pushoutDesc_left [Algebra.IsPushout R S R' S'] {A : Type*} [Semiring A] [Algebra R A] (f : S →ₐ[R] A)
    (g : R' →ₐ[R] A) (H) (x : S) : Algebra.pushoutDesc S' f g H (algebraMap S S' x) = f x := by
  simp [Algebra.pushoutDesc_apply]

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