subalgebraMap_coe_apply — Mathlib

English

If f: A → B is an injective algebra homomorphism, then there is an isomorphism of algebras between S and S.map f for any S ⊆ A, provided via an injective mapping.

Русский

Пусть f: A → B — инъективный алгебра-хомоморфизм. Тогда для любой S ⊆ A существует изоморфизм алгебр между S и S.map f, заданный инъективно.

LaTeX

$$$\text{equivMapOfInjective}(S,f,\ hf) : S \cong_R S.map f$$$

Lean4

@[simp]
theorem _root_.AlgHom.subalgebraMap_coe_apply (x : S) : f.subalgebraMap S x = f x :=
  rfl

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