autCongr_trans

Mathlib.Algebra.Algebra.Equiv

URI: https://scilib.ai/kg/mathlib#AlgEquiv.autCongr_trans

English

AutCongr respects composition: autCongr φ trans autCongr ψ = autCongr (φ trans ψ).

Русский

AutCongr сохраняет композицию: autCongr φ.trans ψ = autCongr (φ.trans ψ).

LaTeX

$$$ (autCongr \\varphi).trans (autCongr \\psi) = autCongr (\\varphi.trans \\psi) $$$

Lean4

@[simp]
theorem autCongr_trans (ϕ : A₁ ≃ₐ[R] A₂) (ψ : A₂ ≃ₐ[R] A₃) : (autCongr ϕ).trans (autCongr ψ) = autCongr (ϕ.trans ψ) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru