equiv_symm_algebraMap_right — Mathlib

English

The pushout property is symmetric: Algebra.IsPushout R S R' S' iff Algebra.IsPushout R R' S S'.

Русский

Свойство пушаута симметрично: Algebra.IsPushout R S R' S' эквивалентно Algebra.IsPushout R R' S S'.

LaTeX

$$Algebra.IsPushout.comm$$

Lean4

theorem equiv_symm_algebraMap_right [Algebra.IsPushout R S R' S'] (a : R') :
    (equiv R S R' S').symm (algebraMap R' S' a) = 1 ⊗ₜ a := by
  rw [(equiv R S R' S').symm_apply_eq, equiv_tmul, map_one, one_mul]

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