ofAlgEquiv_apply

Mathlib.Algebra.Star.StarAlgHom

URI: https://scilib.ai/kg/mathlib#StarAlgEquiv.ofAlgEquiv_apply

English

Symm of toAlgEquiv equals toAlgEquiv of symm.

Русский

Симметрия к toAlgEquiv равна toAlgEquiv к симметрии.

LaTeX

$$$$ \operatorname{coe\_toAlgEquiv} (f) : \; \forall x, (f.toAlgEquiv) x = f x. $$$$

Lean4

@[simp]
theorem ofAlgEquiv_apply (f : A ≃ₐ[R] B) (map_star : ∀ x, f (star x) = star (f x)) (x : A) :
    ofAlgEquiv f map_star x = f x :=
  rfl

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

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

Разделы

Аффилиация

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