toUnder_trans — Mathlib

English

The base change of an algebra isomorphism corresponds to the isomorphism of Under objects.

Русский

Базовое изменение изоморфизмов алгебр соответствует изоморфизму объектов Under.

LaTeX

$$$(f \equivₐ[R] g) \Rightarrow (f.toUnder \text{ is } g.toUnder)$$$

Lean4

@[simp]
theorem toUnder_trans {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra R A] [Algebra R B] [Algebra R C]
    (f : A ≃ₐ[R] B) (g : B ≃ₐ[R] C) : (f.trans g).toUnder = f.toUnder ≪≫ g.toUnder :=
  rfl

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