aut — Mathlib

English

An algebra isomorphism induces a group isomorphism between automorphism groups: Aut(A1) → Aut(A2) by conjugation.

Русский

Алгебраизоморфизм индуцирует групповую изоморфность между группами автоморфизмов: Aut(A1) → Aut(A2) конъюгацией.

LaTeX

$$$\\text{autCongr} : (A_1 \\simeq_{R} A_2) \\Rightarrow (A_1 \\simeq_{R} A_1) \\to (A_2 \\simeq_{R} A_2)$$$

Lean4

@[simps -isSimp one mul, stacks 09HR]
instance aut : Group (A₁ ≃ₐ[R] A₁) where
  mul ϕ ψ := ψ.trans ϕ
  mul_assoc _ _ _ := rfl
  one := refl
  one_mul _ := ext fun _ => rfl
  mul_one _ := ext fun _ => rfl
  inv := symm
  inv_mul_cancel ϕ := ext <| symm_apply_apply ϕ

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